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

Theorem syl2an2r 675
Description: syl2anr 590 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 575 . 2 ((𝜑𝜃) → 𝜏)
51, 4syldan 585 1 ((𝜑𝜒) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384
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 198  df-an 385
This theorem is referenced by:  disjxiun  4806  brcogw  5459  funfni  6169  fvelimab  6442  dff3  6562  f1cofveqaeq  6707  grprinvlem  7070  boxcutc  8156  supmax  8580  cantnff  8786  infxpenlem  9087  cfsmolem  9345  fpwwe2lem8  9712  tsken  9829  addmodlteq  12953  hashdifpr  13404  ccatalpha  13564  fsumrev  14795  climcndslem2  14866  climcnds  14867  dvdsprmpweqle  15869  psgnunilem5  18177  sylow1lem2  18278  lbsextlem2  19433  psrlinv  19671  mplsubglem  19708  mpllsslem  19709  evlslem1  19788  cramerimplem1  20767  topbas  21056  clmvz  23189  cssbn  23452  chlcsschl  23455  ovolunlem1a  23554  chtub  25228  gausslemma2dlem1a  25381  2lgslem3a1  25416  2lgslem3b1  25417  2lgslem3c1  25418  2lgslem3d1  25419  2lgsoddprm  25432  uhgrspansubgrlem  26461  usgrres  26479  usgrnbcnvfv  26545  finsumvtxdg2sstep  26736  uspgr2wlkeq  26833  redwlk  26861  pthdivtx  26917  usgr2wlkspthlem2  26946  wwlknvtx  27030  2wlkdlem6  27154  umgr2wlkon  27173  rusgrnumwwlk  27201  clwwlknwwlksnb  27305  clwwnisshclwwsn  27311  clwwlknscsh  27314  clwlknf1oclwwlknlem1  27346  clwlknf1oclwwlknlem1OLD  27347  1wlkdlem2  27416  fusgreghash2wsp  27618  2clwwlklem  27625  2clwwlklemOLD  27626  2clwwlk2clwwlk  27635  2clwwlk2clwwlkOLD  27636  numclwwlk6  27706  ofpreima2  29916  eulerpartlemgvv  30885  wrdsplex  31066  nosupbnd1lem4  32301  scutbdaylt  32366  gneispace  39106  ax6e2ndeqALT  39819  sineq0ALT  39825  setsv  42082  lighneal  42204  sprsymrelfolem2  42412
  Copyright terms: Public domain W3C validator