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 ⊢ (𝜑 → (𝜒 → (𝜃 → 𝜓)))

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  29  ad5ant125OLD  1391  3ecase  1505  3elpr2eq  4872  pssnn  9154  suppeqfsuppbi  9340  infsupprpr  9467  axdc3lem2  10436  ltexprlem7  11028  nn01to3  12966  xrsupsslem  13334  xrinfmsslem  13335  injresinjlem  13821  injresinj  13822  addmodlteq  13984  ssnn0fi  14023  fsuppmapnn0fiubex  14030  fsuppmapnn0fiub0  14031  nn0o1gt2  16440  cshwsidrepswmod0  17155  symgextf1  19492  psgnunilem4  19568  cmpsublem  23537  aalioulem5  26478  gausslemma2dlem0i  27506  2lgsoddprm  27558  axlowdimlem15  29284  nbusgrvtxm1  29707  nb3grprlem1  29708  lfgrwlkprop  30013  frgrnbnb  30622  frgrwopreglem4a  30639  frgrwopreg  30652  nnn1suc  43011  volicorescl  47247  nnmul2  48044  iccpartiltu  48148  odz2prm2pw  48292  prmdvdsfmtnof1lem2  48314  nnsum3primesle9  48536  bgoldbtbndlem1  48547  clnbgrgrim  48676  grtriprop  48683  isgrtri  48685  grimgrtri  48691  grlimgrtri  48745  lindslinindsimp2lem5  49219  elfzolborelfzop1  49276  nn0sumshdiglemB  49377