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  ad5ant125OLD  1382  3ecase  1494  3elpr2eq  4863  pssnn  9133  suppeqfsuppbi  9322  infsupprpr  9449  axdc3lem2  10405  ltexprlem7  10997  nn01to3  12939  xrsupsslem  13307  xrinfmsslem  13308  injresinjlem  13793  injresinj  13794  addmodlteq  13956  ssnn0fi  13995  fsuppmapnn0fiubex  14002  fsuppmapnn0fiub0  14003  nn0o1gt2  16398  cshwsidrepswmod0  17113  symgextf1  19444  psgnunilem4  19520  cmpsublem  23439  aalioulem5  26377  gausslemma2dlem0i  27405  2lgsoddprm  27457  axlowdimlem15  29103  nbusgrvtxm1  29526  nb3grprlem1  29527  lfgrwlkprop  29832  frgrnbnb  30441  frgrwopreglem4a  30458  frgrwopreg  30471  nnn1suc  42845  volicorescl  47091  nnmul2  47888  iccpartiltu  47992  odz2prm2pw  48136  prmdvdsfmtnof1lem2  48158  nnsum3primesle9  48380  bgoldbtbndlem1  48391  clnbgrgrim  48520  grtriprop  48527  isgrtri  48529  grimgrtri  48535  grlimgrtri  48589  lindslinindsimp2lem5  49048  elfzolborelfzop1  49105  nn0sumshdiglemB  49206