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  4887  pssnn  9187  suppeqfsuppbi  9396  infsupprpr  9523  axdc3lem2  10470  ltexprlem7  11061  nn01to3  12962  xrsupsslem  13328  xrinfmsslem  13329  injresinjlem  13808  injresinj  13809  addmodlteq  13969  ssnn0fi  14008  fsuppmapnn0fiubex  14015  fsuppmapnn0fiub0  14016  nn0o1gt2  16405  cshwsidrepswmod0  17119  symgextf1  19407  psgnunilem4  19483  cmpsublem  23342  aalioulem5  26301  gausslemma2dlem0i  27332  2lgsoddprm  27384  axlowdimlem15  28940  nbusgrvtxm1  29363  nb3grprlem1  29364  lfgrwlkprop  29672  frgrnbnb  30279  frgrwopreglem4a  30296  frgrwopreg  30309  nnn1suc  42283  volicorescl  46549  iccpartiltu  47403  odz2prm2pw  47544  prmdvdsfmtnof1lem2  47566  nnsum3primesle9  47775  bgoldbtbndlem1  47786  clnbgrgrim  47914  grtriprop  47920  isgrtri  47922  grimgrtri  47928  grlimgrtri  47975  lindslinindsimp2lem5  48405  elfzolborelfzop1  48462  nn0sumshdiglemB  48567