Theorem 2a1d 26

Description: Deduction introducing two antecedents. Two applications of a1d 25. Deduction associated with 2a1 28 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 25	. 2 ⊢ (𝜑 → (𝜃 → 𝜓))
3	2	a1d 25	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  28  ad5ant125  1368  3ecase  1476  3elpr2eq  4873  pssnn  9138  suppeqfsuppbi  9337  infsupprpr  9464  axdc3lem2  10411  ltexprlem7  11002  nn01to3  12907  xrsupsslem  13274  xrinfmsslem  13275  injresinjlem  13755  injresinj  13756  addmodlteq  13918  ssnn0fi  13957  fsuppmapnn0fiubex  13964  fsuppmapnn0fiub0  13965  nn0o1gt2  16358  cshwsidrepswmod0  17072  symgextf1  19358  psgnunilem4  19434  cmpsublem  23293  aalioulem5  26251  gausslemma2dlem0i  27282  2lgsoddprm  27334  axlowdimlem15  28890  nbusgrvtxm1  29313  nb3grprlem1  29314  lfgrwlkprop  29622  frgrnbnb  30229  frgrwopreglem4a  30246  frgrwopreg  30259  nnn1suc  42261  volicorescl  46558  iccpartiltu  47427  odz2prm2pw  47568  prmdvdsfmtnof1lem2  47590  nnsum3primesle9  47799  bgoldbtbndlem1  47810  clnbgrgrim  47938  grtriprop  47944  isgrtri  47946  grimgrtri  47952  grlimgrtri  47999  lindslinindsimp2lem5  48455  elfzolborelfzop1  48512  nn0sumshdiglemB  48613