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  1364  3ecase  1472  3elpr2eq  4835  pssnn  8913  pssnnOLD  8969  suppeqfsuppbi  9072  infsupprpr  9193  axdc3lem2  10138  ltexprlem7  10729  nn01to3  12610  xrsupsslem  12970  xrinfmsslem  12971  injresinjlem  13435  injresinj  13436  addmodlteq  13594  ssnn0fi  13633  fsuppmapnn0fiubex  13640  fsuppmapnn0fiub0  13641  nn0o1gt2  16018  cshwsidrepswmod0  16724  symgextf1  18944  psgnunilem4  19020  cmpsublem  22458  aalioulem5  25401  gausslemma2dlem0i  26417  2lgsoddprm  26469  axlowdimlem15  27227  nbusgrvtxm1  27649  nb3grprlem1  27650  lfgrwlkprop  27957  frgrnbnb  28558  frgrwopreglem4a  28575  frgrwopreg  28588  nnn1suc  40217  volicorescl  43981  iccpartiltu  44762  odz2prm2pw  44903  prmdvdsfmtnof1lem2  44925  nnsum3primesle9  45134  bgoldbtbndlem1  45145  lindslinindsimp2lem5  45691  elfzolborelfzop1  45748  nn0sumshdiglemB  45854