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  4860  pssnn  9092  suppeqfsuppbi  9288  infsupprpr  9415  axdc3lem2  10364  ltexprlem7  10955  nn01to3  12860  xrsupsslem  13227  xrinfmsslem  13228  injresinjlem  13708  injresinj  13709  addmodlteq  13871  ssnn0fi  13910  fsuppmapnn0fiubex  13917  fsuppmapnn0fiub0  13918  nn0o1gt2  16310  cshwsidrepswmod0  17024  symgextf1  19318  psgnunilem4  19394  cmpsublem  23302  aalioulem5  26260  gausslemma2dlem0i  27291  2lgsoddprm  27343  axlowdimlem15  28919  nbusgrvtxm1  29342  nb3grprlem1  29343  lfgrwlkprop  29649  frgrnbnb  30255  frgrwopreglem4a  30272  frgrwopreg  30285  nnn1suc  42239  volicorescl  46535  iccpartiltu  47407  odz2prm2pw  47548  prmdvdsfmtnof1lem2  47570  nnsum3primesle9  47779  bgoldbtbndlem1  47790  clnbgrgrim  47919  grtriprop  47926  isgrtri  47928  grimgrtri  47934  grlimgrtri  47988  lindslinindsimp2lem5  48448  elfzolborelfzop1  48505  nn0sumshdiglemB  48606