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  4870  pssnn  9132  suppeqfsuppbi  9330  infsupprpr  9457  axdc3lem2  10404  ltexprlem7  10995  nn01to3  12900  xrsupsslem  13267  xrinfmsslem  13268  injresinjlem  13748  injresinj  13749  addmodlteq  13911  ssnn0fi  13950  fsuppmapnn0fiubex  13957  fsuppmapnn0fiub0  13958  nn0o1gt2  16351  cshwsidrepswmod0  17065  symgextf1  19351  psgnunilem4  19427  cmpsublem  23286  aalioulem5  26244  gausslemma2dlem0i  27275  2lgsoddprm  27327  axlowdimlem15  28883  nbusgrvtxm1  29306  nb3grprlem1  29307  lfgrwlkprop  29615  frgrnbnb  30222  frgrwopreglem4a  30239  frgrwopreg  30252  nnn1suc  42254  volicorescl  46551  iccpartiltu  47423  odz2prm2pw  47564  prmdvdsfmtnof1lem2  47586  nnsum3primesle9  47795  bgoldbtbndlem1  47806  clnbgrgrim  47934  grtriprop  47940  isgrtri  47942  grimgrtri  47948  grlimgrtri  47995  lindslinindsimp2lem5  48451  elfzolborelfzop1  48508  nn0sumshdiglemB  48609