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  1362  3ecase  1470  3elpr2eq  4831  supp0cosupp0OLD  7867  imacosuppOLD  7869  pssnn  8730  suppeqfsuppbi  8841  infsupprpr  8962  axdc3lem2  9867  ltexprlem7  10458  nn01to3  12335  xrsupsslem  12694  xrinfmsslem  12695  injresinjlem  13151  injresinj  13152  addmodlteq  13308  ssnn0fi  13347  fsuppmapnn0fiubex  13354  fsuppmapnn0fiub0  13355  nn0o1gt2  15726  cshwsidrepswmod0  16422  symgextf1  18543  psgnunilem4  18619  cmpsublem  22001  aalioulem5  24919  gausslemma2dlem0i  25934  2lgsoddprm  25986  axlowdimlem15  26736  nbusgrvtxm1  27155  nb3grprlem1  27156  lfgrwlkprop  27463  frgrnbnb  28066  frgrwopreglem4a  28083  frgrwopreg  28096  nnn1suc  39152  volicorescl  42828  iccpartiltu  43575  odz2prm2pw  43718  prmdvdsfmtnof1lem2  43740  nnsum3primesle9  43952  bgoldbtbndlem1  43963  lindslinindsimp2lem5  44510  elfzolborelfzop1  44567  nn0sumshdiglemB  44673