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

Theorem syl2an2r 871
Description: syl2anr 493 with antecedents in standard conjunction form. (Contributed by Alan Sare, 27-Aug-2016.)
Hypotheses
Ref Expression
syl2an2r.1 (𝜑𝜓)
syl2an2r.2 ((𝜑𝜒) → 𝜃)
syl2an2r.3 ((𝜓𝜃) → 𝜏)
Assertion
Ref Expression
syl2an2r ((𝜑𝜒) → 𝜏)

Proof of Theorem syl2an2r
StepHypRef Expression
1 syl2an2r.1 . . 3 (𝜑𝜓)
2 syl2an2r.2 . . 3 ((𝜑𝜒) → 𝜃)
3 syl2an2r.3 . . 3 ((𝜓𝜃) → 𝜏)
41, 2, 3syl2an 492 . 2 ((𝜑 ∧ (𝜑𝜒)) → 𝜏)
54anabss5 852 1 ((𝜑𝜒) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 195  df-an 384
This theorem is referenced by:  disjxiun  4573  brcogw  5200  ordtr3OLD  5673  funfni  5891  fvelimab  6148  dff3  6265  cantnff  8431  infxpenlem  8696  cfsmolem  8952  addmodlteq  12562  hashdifpr  13016  ccatalpha  13174  dvdsprmpweqle  15374  sylow1lem2  17783  lbsextlem2  18926  psrlinv  19164  mplsubglem  19201  mpllsslem  19202  evlslem1  19282  clmvz  22650  gausslemma2dlem1a  24807  2lgslem3a1  24842  2lgslem3b1  24843  2lgslem3c1  24844  2lgslem3d1  24845  2lgsoddprm  24858  ofpreima2  28655  gneispace  37255  ax6e2ndeqALT  37992  sineq0ALT  37998  lighneal  39871  f1cofveqaeq  40139  uspgr2wlkeq  40856  red1wlk  40883  pthdivtx  40937  usgr2wlkspthlem2  40966  21wlkdlem6  41140  umgr2wlkon  41159  rusgrnumwwlk  41180  clwwlksnscsh  41249  11wlkdlem2  41307  fusgreghash2wsp  41504  av-numclwwlkovf2ex  41519  av-numclwwlk6  41546
  Copyright terms: Public domain W3C validator