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  4876  pssnn  9163  suppeqfsuppbi  9349  infsupprpr  9476  axdc3lem2  10453  ltexprlem7  11045  nn01to3  12983  xrsupsslem  13351  xrinfmsslem  13352  injresinjlem  13838  injresinj  13839  addmodlteq  14002  ssnn0fi  14041  fsuppmapnn0fiubex  14048  fsuppmapnn0fiub0  14049  nn0o1gt2  16464  cshwsidrepswmod0  17179  symgextf1  19522  psgnunilem4  19598  cmpsublem  23593  aalioulem5  26536  gausslemma2dlem0i  27565  2lgsoddprm  27617  axlowdimlem15  29343  nbusgrvtxm1  29766  nb3grprlem1  29767  lfgrwlkprop  30072  frgrnbnb  30681  frgrwopreglem4a  30698  frgrwopreg  30711  nnn1suc  43074  volicorescl  47308  nnmul2  48108  iccpartiltu  48212  odz2prm2pw  48356  prmdvdsfmtnof1lem2  48378  nnsum3primesle9  48600  bgoldbtbndlem1  48611  clnbgrgrim  48740  grtriprop  48747  isgrtri  48749  grimgrtri  48755  grlimgrtri  48809  lindslinindsimp2lem5  49283  elfzolborelfzop1  49340  nn0sumshdiglemB  49441