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  4866  pssnn  9168  suppeqfsuppbi  9355  infsupprpr  9482  axdc3lem2  10510  ltexprlem7  11108  nn01to3  13049  xrsupsslem  13418  xrinfmsslem  13419  injresinjlem  13905  injresinj  13906  addmodlteq  14069  ssnn0fi  14108  fsuppmapnn0fiubex  14115  fsuppmapnn0fiub0  14116  nn0o1gt2  16531  cshwsidrepswmod0  17252  symgextf1  19615  psgnunilem4  19691  cmpsublem  23697  aalioulem5  26645  gausslemma2dlem0i  27673  2lgsoddprm  27725  axlowdimlem15  29516  nbusgrvtxm1  29942  nb3grprlem1  29943  lfgrwlkprop  30252  frgrnbnb  30876  frgrwopreglem4a  30893  frgrwopreg  30906  nnn1suc  43299  volicorescl  47507  nnmul2  48344  iccpartiltu  48448  odz2prm2pw  48592  prmdvdsfmtnof1lem2  48614  nnsum3primesle9  48836  bgoldbtbndlem1  48847  clnbgrgrim  48976  grtriprop  48983  isgrtri  48985  grimgrtri  48991  grlimgrtri  49045  lindslinindsimp2lem5  49518  elfzolborelfzop1  49575  nn0sumshdiglemB  49676