Theorem 2a1d 26

Description: Deduction introducing two antecedents. Two applications of a1d 25. Deduction associated with 2a1 28 and 2a1i 12. (Contributed by BJ, 10-Aug-2020.)

Hypothesis

Ref	Expression
2a1d.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
2a1d	⊢ (𝜑 → (𝜒 → (𝜃 → 𝜓)))

Proof of Theorem 2a1d

Step	Hyp	Ref	Expression
1		2a1d.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	a1d 25	. 2 ⊢ (𝜑 → (𝜃 → 𝜓))
3	2	a1d 25	1 ⊢ (𝜑 → (𝜒 → (𝜃 → 𝜓)))

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is referenced by:  2a1  28  ad4ant14  1293  ad5ant145  1315  3ecase  1437  3elpr2eq  4435  supp0cosupp0  7334  imacosupp  7335  pssnn  8178  suppeqfsuppbi  8289  axdc3lem2  9273  ltexprlem7  9864  xrsupsslem  12137  xrinfmsslem  12138  injresinjlem  12588  injresinj  12589  addmodlteq  12745  ssnn0fi  12784  fsuppmapnn0fiubex  12792  fsuppmapnn0fiub0  12793  nn0o1gt2  15097  cshwsidrepswmod0  15801  symgextf1  17841  psgnunilem4  17917  cmpsublem  21202  aalioulem5  24091  gausslemma2dlem0i  25089  2lgsoddprm  25141  axlowdimlem15  25836  nbusgrvtxm1  26281  nb3grprlem1  26282  lfgrwlkprop  26584  frgrnbnb  27157  frgrwopreglem4a  27174  frgrwopreg  27187  numclwwlkffin0  27215  volicorescl  40767  iccpartiltu  41358  odz2prm2pw  41475  prmdvdsfmtnof1lem2  41497  nnsum3primesle9  41682  bgoldbtbndlem1  41693  lindslinindsimp2lem5  42251  elfzolborelfzop1  42309  nn0sumshdiglemB  42414