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  1369  3ecase  1477  3elpr2eq  4850  pssnn  9096  suppeqfsuppbi  9285  infsupprpr  9412  axdc3lem2  10364  ltexprlem7  10956  nn01to3  12882  xrsupsslem  13250  xrinfmsslem  13251  injresinjlem  13736  injresinj  13737  addmodlteq  13899  ssnn0fi  13938  fsuppmapnn0fiubex  13945  fsuppmapnn0fiub0  13946  nn0o1gt2  16341  cshwsidrepswmod0  17056  symgextf1  19387  psgnunilem4  19463  cmpsublem  23374  aalioulem5  26313  gausslemma2dlem0i  27341  2lgsoddprm  27393  axlowdimlem15  29039  nbusgrvtxm1  29462  nb3grprlem1  29463  lfgrwlkprop  29769  frgrnbnb  30378  frgrwopreglem4a  30395  frgrwopreg  30408  nnn1suc  42718  volicorescl  46999  nnmul2  47790  iccpartiltu  47894  odz2prm2pw  48038  prmdvdsfmtnof1lem2  48060  nnsum3primesle9  48282  bgoldbtbndlem1  48293  clnbgrgrim  48422  grtriprop  48429  isgrtri  48431  grimgrtri  48437  grlimgrtri  48491  lindslinindsimp2lem5  48950  elfzolborelfzop1  49007  nn0sumshdiglemB  49108