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  4862  pssnn  9093  suppeqfsuppbi  9282  infsupprpr  9409  axdc3lem2  10361  ltexprlem7  10953  nn01to3  12854  xrsupsslem  13222  xrinfmsslem  13223  injresinjlem  13706  injresinj  13707  addmodlteq  13869  ssnn0fi  13908  fsuppmapnn0fiubex  13915  fsuppmapnn0fiub0  13916  nn0o1gt2  16308  cshwsidrepswmod0  17022  symgextf1  19350  psgnunilem4  19426  cmpsublem  23343  aalioulem5  26300  gausslemma2dlem0i  27331  2lgsoddprm  27383  axlowdimlem15  29029  nbusgrvtxm1  29452  nb3grprlem1  29453  lfgrwlkprop  29759  frgrnbnb  30368  frgrwopreglem4a  30385  frgrwopreg  30398  nnn1suc  42517  volicorescl  46793  iccpartiltu  47664  odz2prm2pw  47805  prmdvdsfmtnof1lem2  47827  nnsum3primesle9  48036  bgoldbtbndlem1  48047  clnbgrgrim  48176  grtriprop  48183  isgrtri  48185  grimgrtri  48191  grlimgrtri  48245  lindslinindsimp2lem5  48704  elfzolborelfzop1  48761  nn0sumshdiglemB  48862