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  1366  3ecase  1474  3elpr2eq  4930  pssnn  9234  suppeqfsuppbi  9448  infsupprpr  9573  axdc3lem2  10520  ltexprlem7  11111  nn01to3  13006  xrsupsslem  13369  xrinfmsslem  13370  injresinjlem  13837  injresinj  13838  addmodlteq  13997  ssnn0fi  14036  fsuppmapnn0fiubex  14043  fsuppmapnn0fiub0  14044  nn0o1gt2  16429  cshwsidrepswmod0  17142  symgextf1  19463  psgnunilem4  19539  cmpsublem  23428  aalioulem5  26396  gausslemma2dlem0i  27426  2lgsoddprm  27478  axlowdimlem15  28989  nbusgrvtxm1  29414  nb3grprlem1  29415  lfgrwlkprop  29723  frgrnbnb  30325  frgrwopreglem4a  30342  frgrwopreg  30355  nnn1suc  42255  volicorescl  46474  iccpartiltu  47296  odz2prm2pw  47437  prmdvdsfmtnof1lem2  47459  nnsum3primesle9  47668  bgoldbtbndlem1  47679  clnbgrgrim  47786  grtriprop  47792  isgrtri  47794  grimgrtri  47798  grlimgrtri  47820  lindslinindsimp2lem5  48191  elfzolborelfzop1  48248  nn0sumshdiglemB  48354