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  1365  3ecase  1473  3elpr2eq  4838  pssnn  8951  pssnnOLD  9040  suppeqfsuppbi  9142  infsupprpr  9263  axdc3lem2  10207  ltexprlem7  10798  nn01to3  12681  xrsupsslem  13041  xrinfmsslem  13042  injresinjlem  13507  injresinj  13508  addmodlteq  13666  ssnn0fi  13705  fsuppmapnn0fiubex  13712  fsuppmapnn0fiub0  13713  nn0o1gt2  16090  cshwsidrepswmod0  16796  symgextf1  19029  psgnunilem4  19105  cmpsublem  22550  aalioulem5  25496  gausslemma2dlem0i  26512  2lgsoddprm  26564  axlowdimlem15  27324  nbusgrvtxm1  27746  nb3grprlem1  27747  lfgrwlkprop  28055  frgrnbnb  28657  frgrwopreglem4a  28674  frgrwopreg  28687  nnn1suc  40296  volicorescl  44091  iccpartiltu  44874  odz2prm2pw  45015  prmdvdsfmtnof1lem2  45037  nnsum3primesle9  45246  bgoldbtbndlem1  45257  lindslinindsimp2lem5  45803  elfzolborelfzop1  45860  nn0sumshdiglemB  45966