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  4799  supp0cosupp0OLD  7856  imacosuppOLD  7858  pssnn  8720  suppeqfsuppbi  8831  infsupprpr  8952  axdc3lem2  9862  ltexprlem7  10453  nn01to3  12329  xrsupsslem  12688  xrinfmsslem  12689  injresinjlem  13152  injresinj  13153  addmodlteq  13309  ssnn0fi  13348  fsuppmapnn0fiubex  13355  fsuppmapnn0fiub0  13356  nn0o1gt2  15722  cshwsidrepswmod0  16420  symgextf1  18541  psgnunilem4  18617  cmpsublem  22004  aalioulem5  24932  gausslemma2dlem0i  25948  2lgsoddprm  26000  axlowdimlem15  26750  nbusgrvtxm1  27169  nb3grprlem1  27170  lfgrwlkprop  27477  frgrnbnb  28078  frgrwopreglem4a  28095  frgrwopreg  28108  nnn1suc  39467  volicorescl  43192  iccpartiltu  43939  odz2prm2pw  44080  prmdvdsfmtnof1lem2  44102  nnsum3primesle9  44312  bgoldbtbndlem1  44323  lindslinindsimp2lem5  44871  elfzolborelfzop1  44928  nn0sumshdiglemB  45034