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  1387  3ecase  1498  3elpr2eq  4866  pssnn  9141  suppeqfsuppbi  9327  infsupprpr  9454  axdc3lem2  10423  ltexprlem7  11015  nn01to3  12953  xrsupsslem  13321  xrinfmsslem  13322  injresinjlem  13807  injresinj  13808  addmodlteq  13970  ssnn0fi  14009  fsuppmapnn0fiubex  14016  fsuppmapnn0fiub0  14017  nn0o1gt2  16427  cshwsidrepswmod0  17142  symgextf1  19479  psgnunilem4  19555  cmpsublem  23513  aalioulem5  26454  gausslemma2dlem0i  27482  2lgsoddprm  27534  axlowdimlem15  29211  nbusgrvtxm1  29634  nb3grprlem1  29635  lfgrwlkprop  29940  frgrnbnb  30549  frgrwopreglem4a  30566  frgrwopreg  30579  nnn1suc  42888  volicorescl  47126  nnmul2  47923  iccpartiltu  48027  odz2prm2pw  48171  prmdvdsfmtnof1lem2  48193  nnsum3primesle9  48415  bgoldbtbndlem1  48426  clnbgrgrim  48555  grtriprop  48562  isgrtri  48564  grimgrtri  48570  grlimgrtri  48624  lindslinindsimp2lem5  49094  elfzolborelfzop1  49151  nn0sumshdiglemB  49252