Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  2a1d Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 2a1d.1 . . 3 (𝜑𝜓)
21a1d 25 . 2 (𝜑 → (𝜃𝜓))
32a1d 25 1 (𝜑 → (𝜒 → (𝜃𝜓)))
 Colors of variables: wff setvar class 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
 Copyright terms: Public domain W3C validator