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  1363  3ecase  1471  3elpr2eq  4912  pssnn  9206  pssnnOLD  9299  suppeqfsuppbi  9422  infsupprpr  9547  axdc3lem2  10494  ltexprlem7  11085  nn01to3  12977  xrsupsslem  13340  xrinfmsslem  13341  injresinjlem  13807  injresinj  13808  addmodlteq  13966  ssnn0fi  14005  fsuppmapnn0fiubex  14012  fsuppmapnn0fiub0  14013  nn0o1gt2  16383  cshwsidrepswmod0  17097  symgextf1  19419  psgnunilem4  19495  cmpsublem  23394  aalioulem5  26364  gausslemma2dlem0i  27393  2lgsoddprm  27445  axlowdimlem15  28890  nbusgrvtxm1  29315  nb3grprlem1  29316  lfgrwlkprop  29624  frgrnbnb  30226  frgrwopreglem4a  30243  frgrwopreg  30256  nnn1suc  42080  volicorescl  46174  iccpartiltu  46994  odz2prm2pw  47135  prmdvdsfmtnof1lem2  47157  nnsum3primesle9  47366  bgoldbtbndlem1  47377  clnbgrgrim  47481  lindslinindsimp2lem5  47845  elfzolborelfzop1  47902  nn0sumshdiglemB  48008