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

Theorem syl2an2r 911
Description: syl2anr 496 with antecedents in standard conjunction form. (Contributed by Alan Sare, 27-Aug-2016.) (Proof shortened by Wolf Lammen, 28-Mar-2022.)
Hypotheses
Ref Expression
syl2an2r.1 (𝜑𝜓)
syl2an2r.2 ((𝜑𝜒) → 𝜃)
syl2an2r.3 ((𝜓𝜃) → 𝜏)
Assertion
Ref Expression
syl2an2r ((𝜑𝜒) → 𝜏)

Proof of Theorem syl2an2r
StepHypRef Expression
1 syl2an2r.2 . 2 ((𝜑𝜒) → 𝜃)
2 syl2an2r.1 . . 3 (𝜑𝜓)
3 syl2an2r.3 . . 3 ((𝜓𝜃) → 𝜏)
42, 3sylan 489 . 2 ((𝜑𝜃) → 𝜏)
51, 4syldan 488 1 ((𝜑𝜒) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383
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 197  df-an 385
This theorem is referenced by:  disjxiun  4801  brcogw  5446  ordtr3OLD  5931  funfni  6152  fvelimab  6415  dff3  6535  f1cofveqaeq  6678  grprinvlem  7037  boxcutc  8117  supmax  8538  cantnff  8744  infxpenlem  9026  cfsmolem  9284  tsken  9768  addmodlteq  12939  hashdifpr  13395  ccatalpha  13565  dvdsprmpweqle  15792  sylow1lem2  18214  lbsextlem2  19361  psrlinv  19599  mplsubglem  19636  mpllsslem  19637  evlslem1  19717  topbas  20978  clmvz  23111  gausslemma2dlem1a  25289  2lgslem3a1  25324  2lgslem3b1  25325  2lgslem3c1  25326  2lgslem3d1  25327  2lgsoddprm  25340  uhgrspansubgrlem  26381  usgrres  26399  usgrnbcnvfv  26465  finsumvtxdg2sstep  26655  uspgr2wlkeq  26752  redwlk  26779  pthdivtx  26835  usgr2wlkspthlem2  26864  wwlknvtx  26948  2wlkdlem6  27051  umgr2wlkon  27070  rusgrnumwwlk  27097  clwwlknwwlksnb  27185  clwwnisshclwwsn  27190  clwwlknscsh  27193  clwlknf1oclwwlknlem1  27225  1wlkdlem2  27290  fusgreghash2wsp  27492  2clwwlklem  27500  2clwwlk2clwwlk  27507  numclwwlk6  27558  ofpreima2  29775  eulerpartlemgvv  30747  nosupbnd1lem4  32163  scutbdaylt  32228  gneispace  38934  ax6e2ndeqALT  39666  sineq0ALT  39672  setsv  41858  lighneal  42038  sprsymrelfolem2  42253
  Copyright terms: Public domain W3C validator