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

Theorem syl2an2r 681
Description: syl2anr 596 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 580 . 2 ((𝜑𝜃) → 𝜏)
51, 4syldan 591 1 ((𝜑𝜒) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 208  df-an 397
This theorem is referenced by:  disjxiun  5060  axprlem4  5323  brcogw  5738  funfni  6454  fvelimab  6734  dff3  6862  fnex  6975  f1cofveqaeq  7010  f1eqcocnv  7051  caofid0l  7427  caofid0r  7428  caofid1  7429  caofid2  7430  onmindif2  7515  limsssuc  7553  fnse  7818  iinon  7968  smoord  7993  smoword  7994  tfrlem11  8015  boxcutc  8494  f1domg  8518  phpeqd  8695  findcard3  8750  unfilem1  8771  f1opwfi  8817  marypha2  8892  supmax  8920  infmin  8947  ordtypelem6  8976  oiexg  8988  oien  8991  cantnff  9126  cantnfp1lem3  9132  cantnflem1b  9138  cantnflem1  9141  opwf  9230  rankopb  9270  xpnum  9369  infxpenlem  9428  infxp  9626  cflim2  9674  cofsmo  9680  cfsmolem  9681  cfcoflem  9683  ssfin3ds  9741  isf34lem5  9789  isf34lem6  9791  isfin1-3  9797  axcc3  9849  alephval2  9983  fpwwe2lem8  10048  canthp1  10065  tsken  10165  ltaddpr  10445  dedekind  10792  recextlem2  11260  recex  11261  gt0div  11495  ge0div  11496  lerec2  11517  uzwo2  12301  infssuzcl  12321  qmulcl  12356  xnegdi  12631  xmulpnf1n  12661  xadddi2  12680  fzm1  12977  2submod  13290  addmodlteq  13304  expnlbnd  13584  faclbnd5  13648  hasheni  13698  hashdifpr  13766  hashgt23el  13775  ccatrn  13933  ccatalpha  13937  swrds1  14018  swrdccat2  14021  ccatpfx  14053  swrdccatin2  14081  pfxccatin12lem2  14083  revccat  14118  revrev  14119  swrdco  14189  relexpindlem  14412  resqrex  14600  fzomaxdiflem  14692  climconst  14890  serf0  15027  fsumf1o  15070  fsumrev  15124  fsumabs  15146  cvgcmp  15161  binomlem  15174  isumshft  15184  climcndslem1  15194  climcndslem2  15195  climcnds  15196  supcvg  15201  fprodcl2lem  15294  tanneg  15491  rpnnen2lem11  15567  modm1div  15609  fzo0dvdseq  15663  bitsfzolem  15773  gcdcllem3  15840  hashdvds  16102  prmdivdiv  16114  reumodprminv  16131  nnnn0modprm0  16133  pythagtrip  16161  dvdsprmpweqle  16212  pockthg  16232  4sqlem9  16272  vdwmc2  16305  vdwlem2  16308  imasaddflem  16793  acsfn1  16922  acsfn1c  16923  acsfn2  16924  oppccofval  16976  diag2  17485  grprinvlem  17872  issubmnd  17926  imasmnd  17937  pwsco2mhm  17980  gsumwspan  17994  frmdss2  18011  grpinvssd  18106  pwssub  18143  imasgrp  18145  subginv  18216  subginvcl  18218  ghmpreima  18310  conjnsg  18324  gass  18361  gsmsymgreqlem2  18479  f1omvdmvd  18491  symgsssg  18515  symgfisg  18516  symgtrinv  18520  psgnunilem5  18542  sylow1lem2  18644  odcau  18649  sylow2  18671  efgsp1  18783  frgpuptf  18816  frgpuptinv  18817  frgpupf  18819  frgpup3lem  18823  mulgdi  18867  gsumval3eu  18944  gsumzsplit  18967  gsumzmhm  18977  gsumxp2  19020  prdsgsum  19021  fsfnn0gsumfsffz  19023  ablfaclem3  19129  srgbinomlem  19214  gsummgp0  19278  imasring  19289  dvdsr01  19325  subrgcrng  19459  subrginv  19471  abv1z  19523  lcomfsupp  19594  lmodvneg1  19597  lspsn  19694  lmhmco  19735  lmhmima  19739  lmhmpreima  19740  reslmhm  19744  lbsextlem2  19851  lidl0cl  19904  aspval2  20046  psrlinv  20096  mplsubglem  20133  mpllsslem  20134  evlslem4  20206  evlslem1  20213  mpfind  20237  evls1rhm  20402  znfld  20623  ipassr2  20707  ocvin  20734  pjfo  20775  obsne0  20785  frlmgsum  20832  madetsumid  20986  scmatcrng  21046  mdetleib2  21113  cramerimplem1  21208  m2pmfzgsumcl  21272  decpmatmul  21296  pmatcollpwscmat  21315  idpm2idmp  21325  pm2mpmhmlem1  21342  chpscmatgsummon  21369  chfacfscmulgsum  21384  chfacfpmmulgsum  21388  topbas  21496  uncld  21565  incld  21567  elcls  21597  neiptopnei  21656  resttopon  21685  restdis  21702  cnclima  21792  paste  21818  cncmp  21916  clsconn  21954  conncompcld  21958  1stcfb  21969  2ndcsb  21973  2ndcredom  21974  kgencmp2  22070  txss12  22129  qtoptop2  22223  qtoptopon  22228  hmphindis  22321  uffixfr  22447  ufildr  22455  isfcls2  22537  tgplacthmeo  22627  tsmsgsum  22662  tgptsmscld  22674  tsmssplit  22675  ustuqtop5  22769  uspreg  22798  prdsxmetlem  22893  prdsbl  23016  metss  23033  metrest  23049  nrmmetd  23099  isngp2  23121  ngpsubcan  23138  lssnlm  23225  nmoid  23266  opnreen  23354  evth  23478  htpyco2  23498  phtpyco2  23509  clmvz  23630  tcphcph  23755  iscmet3  23811  metcld  23824  bcthlem2  23843  cssbn  23893  chlcsschl  23896  minveclem1  23942  evthicc2  23976  ovolunlem1a  24012  ovolicc2lem1  24033  ovolicc2lem4  24036  ovolicc2lem5  24037  uniioombllem2  24099  uniioombllem3  24101  vitalilem2  24125  vitalilem4  24127  vitalilem5  24128  itg2monolem1  24266  cpnres  24449  rolle  24502  dvlip2  24507  dvivthlem2  24521  dvfsumrlimge0  24542  deg1pwle  24628  plydivlem4  24800  ulm0  24894  efif1olem1  25039  efif1olem2  25040  eflogeq  25098  argimlt0  25109  logrec  25254  relogbcxp  25276  atanlogadd  25405  atanlogsub  25407  atantan  25414  ftalem4  25567  ftalem5  25568  basellem3  25574  chtub  25702  dchrpt  25757  dchrsum2  25758  gausslemma2dlem1a  25855  2lgslem3a1  25890  2lgslem3b1  25891  2lgslem3c1  25892  2lgslem3d1  25893  2lgsoddprm  25906  dchrisumlem2  25980  pntrsumbnd2  26057  cnvmot  26241  tglineneq  26344  midexlem  26392  midex  26437  axlowdimlem14  26655  uhgrspansubgrlem  26986  usgrres  27004  usgrnbcnvfv  27061  finsumvtxdg2sstep  27245  uspgr2wlkeq  27341  redwlk  27368  pthdivtx  27424  usgr2wlkspthlem2  27453  wwlknvtx  27537  2wlkdlem6  27624  umgr2wlkon  27643  rusgrnumwwlk  27668  clwwlkwwlksb  27747  clwwlknwwlksnb  27748  clwwnisshclwwsn  27752  clwwlknscsh  27755  clwlknf1oclwwlknlem1  27774  1wlkdlem2  27831  fusgreghash2wsp  28031  2clwwlklem  28036  2clwwlk2clwwlk  28043  numclwwlk6  28083  ofrn2  30302  ofpreima2  30326  wrdsplex  30528  ccatf1  30539  cycpmco2lem5  30686  cycpmco2lem6  30687  cycpmco2lem7  30688  cycpmco2  30689  cyc3co2  30696  imaslmod  30836  rspsnel  30850  qsidomlem1  30869  qsidomlem2  30870  dimpropd  30893  lbsdiflsp0  30908  extdg1id  30939  eulerpartlemgvv  31520  pfxwlk  32254  revwlk  32255  pthhashvtx  32258  spthcycl  32260  umgracycusgr  32285  satfvsucsuc  32496  frrlem13  33019  nosupbnd1lem4  33095  scutbdaylt  33160  cnambfre  34807  frlmvscadiccat  39010  0prjspn  39135  3cubes  39152  gneispace  40349  rr-phpd  40427  grumnudlem  40486  ax6e2ndeqALT  41130  sineq0ALT  41136  fnresdmss  41289  setsv  43404  sprsymrelfolem2  43487  lighneal  43608  isomuspgrlem2c  43827  lincresunit3  44368  2itscp  44600
  Copyright terms: Public domain W3C validator