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  4849  pssnn  9103  suppeqfsuppbi  9292  infsupprpr  9419  axdc3lem2  10373  ltexprlem7  10965  nn01to3  12891  xrsupsslem  13259  xrinfmsslem  13260  injresinjlem  13745  injresinj  13746  addmodlteq  13908  ssnn0fi  13947  fsuppmapnn0fiubex  13954  fsuppmapnn0fiub0  13955  nn0o1gt2  16350  cshwsidrepswmod0  17065  symgextf1  19396  psgnunilem4  19472  cmpsublem  23364  aalioulem5  26302  gausslemma2dlem0i  27327  2lgsoddprm  27379  axlowdimlem15  29025  nbusgrvtxm1  29448  nb3grprlem1  29449  lfgrwlkprop  29754  frgrnbnb  30363  frgrwopreglem4a  30380  frgrwopreg  30393  nnn1suc  42704  volicorescl  46981  nnmul2  47778  iccpartiltu  47882  odz2prm2pw  48026  prmdvdsfmtnof1lem2  48048  nnsum3primesle9  48270  bgoldbtbndlem1  48281  clnbgrgrim  48410  grtriprop  48417  isgrtri  48419  grimgrtri  48425  grlimgrtri  48479  lindslinindsimp2lem5  48938  elfzolborelfzop1  48995  nn0sumshdiglemB  49096