Theorem 2a1d 27

Description: Deduction introducing two antecedents. Two applications of a1d 26. Deduction associated with 2a1 29 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 26	. 2 ⊢ (𝜑 → (𝜃 → 𝜓))
3	2	a1d 26	1 ⊢ (𝜑 → (𝜒 → (𝜃 → 𝜓)))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  2a1  29  ad5ant125OLD  1392  3ecase  1506  3elpr2eq  4837  pssnn  9215  suppeqfsuppbi  9401  infsupprpr  9528  axdc3lem2  10559  ltexprlem7  11157  nn01to3  13098  xrsupsslem  13467  xrinfmsslem  13468  injresinjlem  13955  injresinj  13956  addmodlteq  14119  ssnn0fi  14158  fsuppmapnn0fiubex  14165  fsuppmapnn0fiub0  14166  nn0o1gt2  16583  cshwsidrepswmod0  17304  symgextf1  19668  psgnunilem4  19744  cmpsublem  23750  aalioulem5  26696  gausslemma2dlem0i  27724  2lgsoddprm  27776  axlowdimlem15  29567  nbusgrvtxm1  29993  nb3grprlem1  29994  lfgrwlkprop  30303  frgrnbnb  30927  frgrwopreglem4a  30944  frgrwopreg  30957  nnn1suc  43535  volicorescl  47778  nnmul2  48615  iccpartiltu  48719  odz2prm2pw  48863  prmdvdsfmtnof1lem2  48885  nnsum3primesle9  49107  bgoldbtbndlem1  49118  clnbgrgrim  49247  grtriprop  49254  isgrtri  49256  grimgrtri  49262  grlimgrtri  49316  lindslinindsimp2lem5  49789  elfzolborelfzop1  49846  nn0sumshdiglemB  49947