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  1367  3ecase  1475  3elpr2eq  4905  pssnn  9209  suppeqfsuppbi  9420  infsupprpr  9545  axdc3lem2  10492  ltexprlem7  11083  nn01to3  12984  xrsupsslem  13350  xrinfmsslem  13351  injresinjlem  13827  injresinj  13828  addmodlteq  13988  ssnn0fi  14027  fsuppmapnn0fiubex  14034  fsuppmapnn0fiub0  14035  nn0o1gt2  16419  cshwsidrepswmod0  17133  symgextf1  19440  psgnunilem4  19516  cmpsublem  23408  aalioulem5  26379  gausslemma2dlem0i  27409  2lgsoddprm  27461  axlowdimlem15  28972  nbusgrvtxm1  29397  nb3grprlem1  29398  lfgrwlkprop  29706  frgrnbnb  30313  frgrwopreglem4a  30330  frgrwopreg  30343  nnn1suc  42306  volicorescl  46573  iccpartiltu  47414  odz2prm2pw  47555  prmdvdsfmtnof1lem2  47577  nnsum3primesle9  47786  bgoldbtbndlem1  47797  clnbgrgrim  47907  grtriprop  47913  isgrtri  47915  grimgrtri  47921  grlimgrtri  47968  lindslinindsimp2lem5  48384  elfzolborelfzop1  48441  nn0sumshdiglemB  48546