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  ad4ant14  1285  ad5ant145  1307  3ecase  1429  supp0cosupp0  7221  imacosupp  7222  pssnn  8063  suppeqfsuppbi  8172  axdc3lem2  9156  ltexprlem7  9743  xrsupsslem  12009  xrinfmsslem  12010  injresinjlem  12450  injresinj  12451  addmodlteq  12607  ssnn0fi  12646  fsuppmapnn0fiubex  12654  fsuppmapnn0fiub0  12655  zeneo  14901  nn0o1gt2  14935  cshwsidrepswmod0  15639  symgextf1  17664  psgnunilem4  17740  cmpsublem  21012  aalioulem5  23895  gausslemma2dlem0i  24889  2lgsoddprm  24941  axlowdimlem15  25636  nbcusgra  25992  uvtxnbgra  26021  3v3e3cycl1  26172  4cycl4v4e  26194  4cycl4dv4e  26196  nbhashuvtx1  26442  rusgrasn  26472  frgranbnb  26547  vdn1frgrav2  26552  vdgfrgragt2  26554  volicorescl  39443  iccpartiltu  39960  odz2prm2pw  40013  prmdvdsfmtnof1lem2  40035  nnsum3primesle9  40210  bgoldbtbndlem1  40221  nbusgrvtxm1  40607  nb3grprlem1  40608  lfgrwlkprop  40896  frgrnbnb  41463  frgrwopreglem4  41484  av-numclwwlkffin0  41513  lindslinindsimp2lem5  42045  elfzolborelfzop1  42103  nn0sumshdiglemB  42212