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  4855  pssnn  9072  suppeqfsuppbi  9257  infsupprpr  9384  axdc3lem2  10333  ltexprlem7  10924  nn01to3  12830  xrsupsslem  13197  xrinfmsslem  13198  injresinjlem  13678  injresinj  13679  addmodlteq  13841  ssnn0fi  13880  fsuppmapnn0fiubex  13887  fsuppmapnn0fiub0  13888  nn0o1gt2  16279  cshwsidrepswmod0  16993  symgextf1  19287  psgnunilem4  19363  cmpsublem  23268  aalioulem5  26225  gausslemma2dlem0i  27256  2lgsoddprm  27308  axlowdimlem15  28888  nbusgrvtxm1  29311  nb3grprlem1  29312  lfgrwlkprop  29618  frgrnbnb  30224  frgrwopreglem4a  30241  frgrwopreg  30254  nnn1suc  42256  volicorescl  46548  iccpartiltu  47420  odz2prm2pw  47561  prmdvdsfmtnof1lem2  47583  nnsum3primesle9  47792  bgoldbtbndlem1  47803  clnbgrgrim  47932  grtriprop  47939  isgrtri  47941  grimgrtri  47947  grlimgrtri  48001  lindslinindsimp2lem5  48461  elfzolborelfzop1  48518  nn0sumshdiglemB  48619