Theorem 2a1d 27

Description: Deduction introducing two antecedents. Two applications of a1d 26. Deduction associated with 2a1 29 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 26	. 2 ⊢ (𝜑 → (𝜃 → 𝜓))
3	2	a1d 26	1 ⊢ (𝜑 → (𝜒 → (𝜃 → 𝜓)))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  2a1  29  ad5ant125OLD  1391  3ecase  1505  3elpr2eq  4833  pssnn  9187  suppeqfsuppbi  9374  infsupprpr  9501  axdc3lem2  10532  ltexprlem7  11130  nn01to3  13071  xrsupsslem  13440  xrinfmsslem  13441  injresinjlem  13928  injresinj  13929  addmodlteq  14092  ssnn0fi  14131  fsuppmapnn0fiubex  14138  fsuppmapnn0fiub0  14139  nn0o1gt2  16556  cshwsidrepswmod0  17277  symgextf1  19640  psgnunilem4  19716  cmpsublem  23722  aalioulem5  26668  gausslemma2dlem0i  27696  2lgsoddprm  27748  axlowdimlem15  29539  nbusgrvtxm1  29965  nb3grprlem1  29966  lfgrwlkprop  30275  frgrnbnb  30899  frgrwopreglem4a  30916  frgrwopreg  30929  nnn1suc  43424  volicorescl  47656  nnmul2  48493  iccpartiltu  48597  odz2prm2pw  48741  prmdvdsfmtnof1lem2  48763  nnsum3primesle9  48985  bgoldbtbndlem1  48996  clnbgrgrim  49125  grtriprop  49132  isgrtri  49134  grimgrtri  49140  grlimgrtri  49194  lindslinindsimp2lem5  49667  elfzolborelfzop1  49724  nn0sumshdiglemB  49825