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  1369  3ecase  1477  3elpr2eq  4864  pssnn  9105  suppeqfsuppbi  9294  infsupprpr  9421  axdc3lem2  10373  ltexprlem7  10965  nn01to3  12866  xrsupsslem  13234  xrinfmsslem  13235  injresinjlem  13718  injresinj  13719  addmodlteq  13881  ssnn0fi  13920  fsuppmapnn0fiubex  13927  fsuppmapnn0fiub0  13928  nn0o1gt2  16320  cshwsidrepswmod0  17034  symgextf1  19362  psgnunilem4  19438  cmpsublem  23355  aalioulem5  26312  gausslemma2dlem0i  27343  2lgsoddprm  27395  axlowdimlem15  29041  nbusgrvtxm1  29464  nb3grprlem1  29465  lfgrwlkprop  29771  frgrnbnb  30380  frgrwopreglem4a  30397  frgrwopreg  30410  nnn1suc  42630  volicorescl  46905  iccpartiltu  47776  odz2prm2pw  47917  prmdvdsfmtnof1lem2  47939  nnsum3primesle9  48148  bgoldbtbndlem1  48159  clnbgrgrim  48288  grtriprop  48295  isgrtri  48297  grimgrtri  48303  grlimgrtri  48357  lindslinindsimp2lem5  48816  elfzolborelfzop1  48873  nn0sumshdiglemB  48974