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  1368  3ecase  1476  3elpr2eq  4858  pssnn  9078  suppeqfsuppbi  9263  infsupprpr  9390  axdc3lem2  10339  ltexprlem7  10930  nn01to3  12836  xrsupsslem  13203  xrinfmsslem  13204  injresinjlem  13687  injresinj  13688  addmodlteq  13850  ssnn0fi  13889  fsuppmapnn0fiubex  13896  fsuppmapnn0fiub0  13897  nn0o1gt2  16289  cshwsidrepswmod0  17003  symgextf1  19331  psgnunilem4  19407  cmpsublem  23312  aalioulem5  26269  gausslemma2dlem0i  27300  2lgsoddprm  27352  axlowdimlem15  28932  nbusgrvtxm1  29355  nb3grprlem1  29356  lfgrwlkprop  29662  frgrnbnb  30268  frgrwopreglem4a  30285  frgrwopreg  30298  nnn1suc  42298  volicorescl  46590  iccpartiltu  47452  odz2prm2pw  47593  prmdvdsfmtnof1lem2  47615  nnsum3primesle9  47824  bgoldbtbndlem1  47835  clnbgrgrim  47964  grtriprop  47971  isgrtri  47973  grimgrtri  47979  grlimgrtri  48033  lindslinindsimp2lem5  48493  elfzolborelfzop1  48550  nn0sumshdiglemB  48651