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  1365  3ecase  1473  3elpr2eq  4911  pssnn  9207  suppeqfsuppbi  9417  infsupprpr  9542  axdc3lem2  10489  ltexprlem7  11080  nn01to3  12981  xrsupsslem  13346  xrinfmsslem  13347  injresinjlem  13823  injresinj  13824  addmodlteq  13984  ssnn0fi  14023  fsuppmapnn0fiubex  14030  fsuppmapnn0fiub0  14031  nn0o1gt2  16415  cshwsidrepswmod0  17129  symgextf1  19454  psgnunilem4  19530  cmpsublem  23423  aalioulem5  26393  gausslemma2dlem0i  27423  2lgsoddprm  27475  axlowdimlem15  28986  nbusgrvtxm1  29411  nb3grprlem1  29412  lfgrwlkprop  29720  frgrnbnb  30322  frgrwopreglem4a  30339  frgrwopreg  30352  nnn1suc  42280  volicorescl  46509  iccpartiltu  47347  odz2prm2pw  47488  prmdvdsfmtnof1lem2  47510  nnsum3primesle9  47719  bgoldbtbndlem1  47730  clnbgrgrim  47840  grtriprop  47846  isgrtri  47848  grimgrtri  47852  grlimgrtri  47899  lindslinindsimp2lem5  48308  elfzolborelfzop1  48365  nn0sumshdiglemB  48470