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  ad5ant125  1366  3ecase  1474  3elpr2eq  4907  pssnn  9170  pssnnOLD  9267  suppeqfsuppbi  9379  infsupprpr  9501  axdc3lem2  10448  ltexprlem7  11039  nn01to3  12927  xrsupsslem  13288  xrinfmsslem  13289  injresinjlem  13754  injresinj  13755  addmodlteq  13913  ssnn0fi  13952  fsuppmapnn0fiubex  13959  fsuppmapnn0fiub0  13960  nn0o1gt2  16326  cshwsidrepswmod0  17030  symgextf1  19291  psgnunilem4  19367  cmpsublem  22910  aalioulem5  25856  gausslemma2dlem0i  26874  2lgsoddprm  26926  axlowdimlem15  28252  nbusgrvtxm1  28674  nb3grprlem1  28675  lfgrwlkprop  28982  frgrnbnb  29584  frgrwopreglem4a  29601  frgrwopreg  29614  nnn1suc  41268  volicorescl  45354  iccpartiltu  46175  odz2prm2pw  46316  prmdvdsfmtnof1lem2  46338  nnsum3primesle9  46547  bgoldbtbndlem1  46558  lindslinindsimp2lem5  47227  elfzolborelfzop1  47284  nn0sumshdiglemB  47390