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  4857  pssnn  9085  suppeqfsuppbi  9270  infsupprpr  9397  axdc3lem2  10349  ltexprlem7  10940  nn01to3  12841  xrsupsslem  13208  xrinfmsslem  13209  injresinjlem  13692  injresinj  13693  addmodlteq  13855  ssnn0fi  13894  fsuppmapnn0fiubex  13901  fsuppmapnn0fiub0  13902  nn0o1gt2  16294  cshwsidrepswmod0  17008  symgextf1  19335  psgnunilem4  19411  cmpsublem  23315  aalioulem5  26272  gausslemma2dlem0i  27303  2lgsoddprm  27355  axlowdimlem15  28936  nbusgrvtxm1  29359  nb3grprlem1  29360  lfgrwlkprop  29666  frgrnbnb  30275  frgrwopreglem4a  30292  frgrwopreg  30305  nnn1suc  42384  volicorescl  46675  iccpartiltu  47546  odz2prm2pw  47687  prmdvdsfmtnof1lem2  47709  nnsum3primesle9  47918  bgoldbtbndlem1  47929  clnbgrgrim  48058  grtriprop  48065  isgrtri  48067  grimgrtri  48073  grlimgrtri  48127  lindslinindsimp2lem5  48587  elfzolborelfzop1  48644  nn0sumshdiglemB  48745