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  1391  3ecase  1505  3elpr2eq  4869  pssnn  9167  suppeqfsuppbi  9353  infsupprpr  9480  axdc3lem2  10457  ltexprlem7  11055  nn01to3  12994  xrsupsslem  13363  xrinfmsslem  13364  injresinjlem  13850  injresinj  13851  addmodlteq  14014  ssnn0fi  14053  fsuppmapnn0fiubex  14060  fsuppmapnn0fiub0  14061  nn0o1gt2  16477  cshwsidrepswmod0  17192  symgextf1  19554  psgnunilem4  19630  cmpsublem  23630  aalioulem5  26579  gausslemma2dlem0i  27608  2lgsoddprm  27660  axlowdimlem15  29421  nbusgrvtxm1  29847  nb3grprlem1  29848  lfgrwlkprop  30157  frgrnbnb  30781  frgrwopreglem4a  30798  frgrwopreg  30811  nnn1suc  43155  volicorescl  47389  nnmul2  48226  iccpartiltu  48330  odz2prm2pw  48474  prmdvdsfmtnof1lem2  48496  nnsum3primesle9  48718  bgoldbtbndlem1  48729  clnbgrgrim  48858  grtriprop  48865  isgrtri  48867  grimgrtri  48873  grlimgrtri  48927  lindslinindsimp2lem5  49400  elfzolborelfzop1  49457  nn0sumshdiglemB  49558