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  4867  pssnn  9141  suppeqfsuppbi  9327  infsupprpr  9454  axdc3lem2  10423  ltexprlem7  11015  nn01to3  12956  xrsupsslem  13324  xrinfmsslem  13325  injresinjlem  13810  injresinj  13811  addmodlteq  13973  ssnn0fi  14012  fsuppmapnn0fiubex  14019  fsuppmapnn0fiub0  14020  nn0o1gt2  16429  cshwsidrepswmod0  17144  symgextf1  19482  psgnunilem4  19558  cmpsublem  23517  aalioulem5  26458  gausslemma2dlem0i  27486  2lgsoddprm  27538  axlowdimlem15  29215  nbusgrvtxm1  29638  nb3grprlem1  29639  lfgrwlkprop  29944  frgrnbnb  30553  frgrwopreglem4a  30570  frgrwopreg  30583  nnn1suc  42893  volicorescl  47125  nnmul2  47922  iccpartiltu  48026  odz2prm2pw  48170  prmdvdsfmtnof1lem2  48192  nnsum3primesle9  48414  bgoldbtbndlem1  48425  clnbgrgrim  48554  grtriprop  48561  isgrtri  48563  grimgrtri  48569  grlimgrtri  48623  lindslinindsimp2lem5  49093  elfzolborelfzop1  49150  nn0sumshdiglemB  49251