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  1374  3ecase  1482  3elpr2eq  4844  pssnn  9100  suppeqfsuppbi  9289  infsupprpr  9416  axdc3lem2  10371  ltexprlem7  10963  nn01to3  12889  xrsupsslem  13257  xrinfmsslem  13258  injresinjlem  13743  injresinj  13744  addmodlteq  13906  ssnn0fi  13945  fsuppmapnn0fiubex  13952  fsuppmapnn0fiub0  13953  nn0o1gt2  16348  cshwsidrepswmod0  17063  symgextf1  19394  psgnunilem4  19470  cmpsublem  23389  aalioulem5  26327  gausslemma2dlem0i  27352  2lgsoddprm  27404  axlowdimlem15  29050  nbusgrvtxm1  29473  nb3grprlem1  29474  lfgrwlkprop  29779  frgrnbnb  30388  frgrwopreglem4a  30405  frgrwopreg  30418  nnn1suc  42756  volicorescl  47003  nnmul2  47800  iccpartiltu  47904  odz2prm2pw  48048  prmdvdsfmtnof1lem2  48070  nnsum3primesle9  48292  bgoldbtbndlem1  48303  clnbgrgrim  48432  grtriprop  48439  isgrtri  48441  grimgrtri  48447  grlimgrtri  48501  lindslinindsimp2lem5  48960  elfzolborelfzop1  49017  nn0sumshdiglemB  49118