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

Theorem syl22anc 1367
Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
Hypotheses
Ref Expression
syl12anc.1 (𝜑𝜓)
syl12anc.2 (𝜑𝜒)
syl12anc.3 (𝜑𝜃)
syl22anc.4 (𝜑𝜏)
syl22anc.5 (((𝜓𝜒) ∧ (𝜃𝜏)) → 𝜂)
Assertion
Ref Expression
syl22anc (𝜑𝜂)

Proof of Theorem syl22anc
StepHypRef Expression
1 syl12anc.1 . . 3 (𝜑𝜓)
2 syl12anc.2 . . 3 (𝜑𝜒)
31, 2jca 553 . 2 (𝜑 → (𝜓𝜒))
4 syl12anc.3 . 2 (𝜑𝜃)
5 syl22anc.4 . 2 (𝜑𝜏)
6 syl22anc.5 . 2 (((𝜓𝜒) ∧ (𝜃𝜏)) → 𝜂)
73, 4, 5, 6syl12anc 1364 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:  preqsnd  4423  fr2nr  5121  soltmin  5567  f1oprg  6219  f1prex  6579  fveqf1o  6597  weniso  6644  fr3nr  7021  smogt  7509  smorndom  7510  oacomf1o  7690  difsnen  8083  undom  8089  enfixsn  8110  domss2  8160  ssenen  8175  marypha1lem  8380  fisupcl  8416  ordtypelem3  8466  ordtypelem8  8471  oieu  8485  oismo  8486  wofib  8491  wemaplem2  8493  wemapso  8497  wemapso2lem  8498  unxpwdom2  8534  infdifsn  8592  oemapvali  8619  cantnflem1c  8622  cantnflem1  8624  cantnf  8628  cnfcom3  8639  r1ordg  8679  dif1card  8871  infxpenlem  8874  dfac8clem  8893  infxp  9075  infmap2  9078  cflim2  9123  coftr  9133  fin2i2  9178  enfin2i  9181  fin23lem26  9185  fin23lem27  9188  fin23lem40  9211  isf32lem2  9214  isf32lem3  9215  isf32lem4  9216  isf32lem7  9219  isf32lem9  9221  fin1a2lem13  9272  fin12  9273  alephexp1  9439  gchdomtri  9489  fpwwe2lem12  9501  fpwwe2lem13  9502  gchpwdom  9530  gchhar  9539  adderpqlem  9814  mulerpqlem  9815  addassnq  9818  mulassnq  9819  distrnq  9821  mulidnq  9823  recmulnq  9824  ltexnq  9835  distrlem1pr  9885  distrlem4pr  9886  prlem936  9907  reclem3pr  9909  mulcmpblnr  9930  mulgt0d  10230  mul4d  10286  add4d  10302  add42d  10303  subcan  10374  addsub4d  10477  subadd4d  10478  sub4d  10479  2addsubd  10480  addsubeq4d  10481  muladdd  10527  mulsubd  10528  addgegt0d  10639  addge0d  10641  mulge0d  10642  le2addd  10684  le2subd  10685  ltleaddd  10686  leltaddd  10687  lt2subd  10689  divdivdiv  10764  divcan5  10765  divne0d  10855  recdivd  10856  recdiv2d  10857  divcan6d  10858  ddcand  10859  rec11d  10860  divmuldivd  10880  divmul13d  10881  divmul24d  10882  divadddivd  10883  divsubdivd  10884  divmuleqd  10885  divdivdivd  10886  subrecd  10894  mulge0b  10931  recreclt  10960  divgt0d  10997  mulgt1d  10998  lemulge11d  10999  lemulge12d  11000  ltmul12ad  11003  lemul12ad  11004  lemul12bd  11005  supmul1  11030  nndivtr  11100  qreccl  11846  ledivdivd  11935  lediv12ad  11969  lt2mul2divd  11977  xlt2add  12128  supxrun  12184  supxrre  12195  infxrre  12204  elicore  12264  iccss2  12282  iccssico2  12285  lincmb01cmp  12353  iccf1o  12354  fzrev2i  12443  fz1fzo0m1  12555  2tnp1ge0ge0  12670  m1modnnsub1  12756  modaddmodup  12773  modaddmodlo  12774  modsubdir  12779  fzennn  12807  sermono  12873  mulexpz  12940  expaddz  12944  ltexp2a  12952  leexp2a  12956  sqdiv  12968  expmulnbnd  13036  digit1  13038  expsubd  13059  lt2sqd  13083  le2sqd  13084  sq11d  13085  bcm1k  13142  bcp1n  13143  bcp1nk  13144  hashf1lem1  13277  cshw1  13614  2swrd2eqwrdeq  13742  ofccat  13754  absrele  14092  sqreulem  14143  sqrtmuld  14207  sqrtsq2d  14208  sqrtled  14209  sqrtltd  14210  sqr11d  14211  abs3lemd  14244  rlimuni  14325  climuni  14327  lo1resb  14339  o1resb  14341  2clim  14347  addcn2  14368  mulcn2  14370  o1of2  14387  o1rlimmul  14393  lo1add  14401  lo1mul  14402  isercolllem1  14439  caucvgrlem  14447  iseraltlem2  14457  iseraltlem3  14458  iseralt  14459  mptfzshft  14554  fsumrev  14555  fsum0diag2  14559  binomlem  14605  climcndslem1  14625  climcndslem2  14626  harmonic  14635  mertenslem1  14660  fprodser  14723  fprodrev  14751  rprisefaccl  14798  efcllem  14852  moddvds  15038  dvds1  15088  dvdsext  15090  oexpneg  15116  evennn02n  15121  evennn2n  15122  bitsinv1  15211  sadaddlem  15235  sadasslem  15239  sadeq  15241  mulgcd  15312  dvdssqlem  15326  lcmftp  15396  rpmulgcd2  15417  coprmproddvdslem  15423  isprm5  15466  isprm6  15473  crth  15530  eulerthlem2  15534  prmdiveq  15538  pythagtriplem11  15577  pythagtriplem13  15579  iserodd  15587  pcgcd1  15628  pcprmpw2  15633  pcaddlem  15639  fldivp1  15648  4sqlem12  15707  4sqlem14  15709  4sqlem15  15710  4sqlem16  15711  vdwapun  15725  mreexexlem4d  16354  acsfn1  16369  acsfn2  16371  sscpwex  16522  rescabs  16540  yonedainv  16968  subm0  17403  pmtrfb  17931  psgnunilem1  17959  odmodnn0  18005  odeq  18015  dfod2  18027  sylow1lem1  18059  lsmsubg  18115  lsmmod  18134  lsmdisj2  18141  ghmplusg  18295  odadd  18299  gexexlem  18301  lt6abl  18342  cyggex2  18344  dprdfinv  18464  dmdprdsplitlem  18482  dpjidcl  18503  ablfacrp  18511  ablfacrp2  18512  ablfac1c  18516  ablfac1eu  18518  lcomfsupp  18951  lssvancl1  18993  lssvnegcl  19004  lspprvacl  19047  lspsneli  19049  lspsn  19050  lmhmplusg  19092  lmhmima  19095  lmhmpreima  19096  reslmhm  19100  lbsind2  19129  lsmcl  19131  lsmelval2  19133  lsppreli  19138  lspprabs  19143  pj1lmhm  19148  lssvs0or  19158  lspabs3  19169  lspfixed  19176  lspexch  19177  lsmcv  19189  lspsolv  19191  lidlmcl  19265  drngnidl  19277  2idlcpbl  19282  mplbas2  19518  evlslem3  19562  evlslem1  19563  coe1addfv  19683  lply1binom  19724  evl1addd  19753  evl1subd  19754  evl1muld  19755  gzrngunit  19860  zringlpirlem3  19882  prmirredlem  19889  znf1o  19948  znunithash  19961  frlmsubgval  20156  frlmvscaval  20158  frlmphllem  20167  frlmphl  20168  frlmssuvc1  20181  frlmsslsp  20183  frlmup1  20185  frlmup2  20186  lindfind2  20205  lindfrn  20208  f1lindf  20209  islindf4  20225  mamudi  20257  mamudir  20258  1marepvmarrepid  20429  mdetrlin  20456  smadiadetglem1  20525  smadiadetg  20527  cramerimplem1  20537  mat2pmatscmxcl  20593  m2pmfzgsumcl  20601  pmatcollpw  20634  pmatcollpwfi  20635  pmatcollpw3fi1lem1  20639  cpmidpmatlem2  20724  cpmadugsumlemF  20729  chcoeffeqlem  20738  ntrin  20913  topssnei  20976  restbas  21010  restntr  21034  cnntri  21123  fiuncmp  21255  nllyrest  21337  nllyidm  21340  hausllycmp  21345  cldllycmp  21346  hauspwdom  21352  txcld  21454  txcn  21477  txlly  21487  txnlly  21488  txhaus  21498  txlm  21499  txkgen  21503  xkococnlem  21510  cnmpt2res  21528  xkoinjcn  21538  basqtop  21562  qtopeu  21567  trfbas2  21694  neifil  21731  hausflim  21832  alexsubALTlem2  21899  cnextfval  21913  cnextfvval  21916  cnextf  21917  cnextfres  21920  clssubg  21959  utop2nei  22101  utop3cls  22102  utopreg  22103  psmetlecl  22167  xmetlecl  22198  prdsxmetlem  22220  bldisj  22250  imasf1obl  22340  prdsbl  22343  stdbdmet  22368  stdbdmopn  22370  met2ndci  22374  metcnp  22393  metustto  22405  metustexhalf  22408  cfilucfil  22411  metucn  22423  lssnlm  22552  nmotri  22590  nmoid  22593  tgioo  22646  blcvx  22648  xrsmopn  22662  reperflem  22668  reconnlem2  22677  opnreen  22681  metdsge  22699  metdsre  22703  metdscnlem  22705  metnrmlem1a  22708  metnrmlem1  22709  metnrmlem3  22711  cncfmet  22758  cnmpt2pc  22774  icopnfcnv  22788  icopnfhmeo  22789  cnllycmp  22802  evth  22805  lebnumii  22812  nmoleub2lem3  22961  iscfil2  23110  cfil3i  23113  iscfil3  23117  cfilfcls  23118  iscau3  23122  iscmet3lem2  23136  caubl  23152  lmcau  23157  rrxcph  23226  minveclem2  23243  pjthlem1  23254  pjthlem2  23255  ivthicc  23273  ovollecl  23297  ovolunlem1a  23310  ovolunnul  23314  ovoliunlem1  23316  ismbl2  23341  nulmbl2  23350  unmbl  23351  volun  23359  voliunlem2  23365  ioombl1lem2  23373  uniioombllem2a  23396  uniioombllem3  23399  uniioombllem4  23400  dyaddisjlem  23409  dyadmaxlem  23411  opnmbllem  23415  volsup2  23419  volcn  23420  ismbfd  23452  mbfi1fseqlem1  23527  mbfi1fseqlem5  23531  itg2lecl  23550  itg2monolem2  23563  itg2gt0  23572  itgspliticc  23648  ellimc3  23688  limcres  23695  dvfval  23706  dvres3  23722  dvres3a  23723  dvnff  23731  dvnadd  23737  dvn2bss  23738  dvnres  23739  dvcmul  23752  dvcmulf  23753  dvmptres3  23764  dvmptres2  23770  dvmptntr  23779  dvexp3  23786  dvferm1lem  23792  dvlip  23801  dvlipcn  23802  dvlip2  23803  c1liplem1  23804  dvgt0lem1  23810  dvgt0lem2  23811  dvne0  23819  lhop1lem  23821  lhop2  23823  lhop  23824  dvcnvrelem1  23825  dvcnvrelem2  23826  dvcvx  23828  dvfsumle  23829  dvfsumabs  23831  dvfsumlem2  23835  ftc1lem6  23849  ftc1  23850  ftc2ditglem  23853  itgsubstlem  23856  tdeglem4  23865  mdegaddle  23879  mdegmullem  23883  ply1rem  23968  fta1glem2  23971  fta1blem  23973  ig1peu  23976  ig1pdvds  23981  dgrmulc  24072  dgrcolem1  24074  plydivlem4  24096  plydiveu  24098  fta1lem  24107  vieta1lem1  24110  vieta1lem2  24111  plyexmo  24113  taylfvallem1  24156  taylfval  24158  tayl0  24161  taylplem1  24162  taylply2  24167  taylply  24168  dvtaylp  24169  dvntaylp  24170  dvntaylp0  24171  taylthlem1  24172  taylthlem2  24173  ulmcaulem  24193  ulmcau  24194  ulmcn  24198  ulmdvlem1  24199  radcnvlem1  24212  radcnvle  24219  psercn  24225  pserdvlem2  24227  pserdv  24228  abelth  24240  cosordlem  24322  tanregt0  24330  dvlog2lem  24443  efopn  24449  logtayllem  24450  logccv  24454  cxplt3  24491  cxpmul2zd  24507  cxpltd  24510  cxpled  24511  cxplt3d  24523  cxple3d  24524  dvsqrt  24528  cxpcn3  24534  cxpaddle  24538  cxpeq  24543  angcan  24577  angvald  24579  ang180lem2  24585  ang180  24589  isosctrlem3  24595  dquartlem1  24623  atantayl2  24710  leibpilem1  24712  leibpi  24714  log2tlbnd  24717  birthdaylem3  24725  xrlimcnp  24740  efrlim  24741  o1cxp  24746  jensenlem2  24759  jensen  24760  fsumharmonic  24783  lgamucov  24809  lgamcvg2  24826  wilthlem1  24839  basellem3  24854  basellem6  24857  basellem8  24859  ppisval  24875  chtwordi  24927  ppiwordi  24933  mumullem2  24951  dvdsmulf1o  24965  fsumvma  24983  fsumvma2  24984  chpchtsum  24989  chpub  24990  logfacubnd  24991  dchrmulcl  25019  dchrinv  25031  dchrptlem1  25034  dchrptlem2  25035  sumdchr2  25040  dchr2sum  25043  bposlem7  25060  lgslem1  25067  lgslem3  25069  lgsdirprm  25101  lgsqrlem2  25117  lgseisenlem1  25145  lgseisenlem2  25146  lgseisenlem4  25148  lgseisen  25149  lgsquadlem1  25150  lgsquad2lem1  25154  lgsquad3  25157  m1lgs  25158  2sqlem7  25194  chebbnd1lem2  25204  chebbnd1lem3  25205  rplogsumlem1  25218  rpvmasumlem  25221  dchrvmasumlem1  25229  dchrvmasum2lem  25230  dchrvmasumlema  25234  dchrisum0flblem2  25243  dchrisum0fno1  25245  dchrisum0re  25247  logdivsum  25267  pntrsumbnd2  25301  pntpbnd1a  25319  pntpbnd1  25320  pntibndlem2  25325  pntlemr  25336  pntlemj  25337  pntlemf  25339  pnt2  25347  padicabv  25364  ostth2lem2  25368  f1otrg  25796  brbtwn2  25830  colinearalglem2  25832  axcgrtr  25840  axcgrid  25841  axsegconlem7  25848  axsegcon  25852  ax5seglem3  25856  ax5seglem6  25859  ax5seg  25863  axpaschlem  25865  axlowdimlem17  25883  axcontlem2  25890  axcontlem4  25892  axcontlem7  25895  axcontlem8  25896  ecgrtg  25908  usgredg2v  26164  vtxdgoddnumeven  26505  2trlond  26904  clwwlknonex2  27084  eupthp1  27194  nmobndi  27758  ubthlem2  27855  ubthlem3  27856  minvecolem2  27859  shuni  28287  pjhthlem1  28378  chscllem2  28625  pjcompi  28659  mayete3i  28715  unoplin  28907  hmoplin  28929  nmophmi  29018  mdslmd4i  29320  isoun  29607  xrge0addcld  29655  xrofsup  29661  eliccelico  29667  elicoelioo  29668  difioo  29672  rexdiv  29762  2sqmod  29776  xrge0addgt0  29819  omndadd2d  29836  omndadd2rd  29837  omndmul2  29840  ofldchr  29942  mdetpmtr2  30018  mdetpmtr12  30019  madjusmdetlem1  30021  madjusmdetlem4  30024  unitdivcld  30075  xrge0mulc1cn  30115  qqhnm  30162  esumcst  30253  esumfsup  30260  esumpmono  30269  esumcvg  30276  difelsiga  30324  sigapisys  30346  sigapildsys  30353  ldgenpisyslem1  30354  1stmbfm  30450  2ndmbfm  30451  dya2icoseg  30467  sibfinima  30529  probmeasb  30620  orvcgteel  30657  orvclteel  30662  ballotlemsima  30705  ballotlemfrceq  30718  sgnmul  30732  ccatmulgnn0dir  30747  fct2relem  30803  ftc2re  30804  chtvalz  30835  subfacp1lem2a  31288  subfaclim  31296  erdsze2lem2  31312  cvmliftlem2  31394  cvmliftlem10  31402  cvmliftlem13  31404  cvmliftiota  31409  cvmlift2lem9  31419  cvmlift2lem11  31421  cvmlift2lem12  31422  cvmliftphtlem  31425  cvmlift3lem6  31432  cvmlift3lem7  31433  cvmlift3lem9  31435  snmlff  31437  mrsubfval  31531  trpredelss  31856  trpredpo  31859  wzel  31894  wsuclem  31895  sltrec  32049  brsegle  32340  opnregcld  32450  addgtge0d  32621  fin2so  33526  poimirlem17  33556  poimirlem23  33562  opnmbllem0  33575  mblfinlem3  33578  mblfinlem4  33579  itg2addnclem  33591  itg2addnc  33594  itg2gt0cn  33595  ftc1cnnclem  33613  ftc1cnnc  33614  areacirclem5  33634  indexdom  33659  sstotbnd2  33703  isbnd3  33713  isbnd3b  33714  cntotbnd  33725  ismtyima  33732  heibor1lem  33738  heiborlem8  33747  rrncmslem  33761  reheibor  33768  lkrlsp  34707  lshpkrlem5  34719  ldualssvscl  34763  ldualssvsubcl  34764  llnmlplnN  35143  llncvrlpln  35162  pmapjat1  35457  pclfinN  35504  lautlt  35695  lauteq  35699  lautco  35701  ltrn11  35730  ltrnle  35733  ltrneq2  35752  cdlemednuN  35905  cdleme20k  35924  cdleme20l2  35926  cdleme20l  35927  cdleme20m  35928  cdleme21c  35932  cdleme22e  35949  cdleme22eALTN  35950  cdlemefrs32fva  36005  cdlemg4g  36221  cdlemg18b  36284  cdlemg18c  36285  cdlemj3  36428  dia2dimlem5  36674  dvhopN  36722  cdlemm10N  36724  dihjatcclem4  37027  dochexmidlem2  37067  lclkrlem2o  37127  lcfrlem5  37152  lcfrlem6  37153  lcdlssvscl  37212  mapdpglem6  37284  mapdpglem9  37286  mapdpglem12  37289  mapdpglem14  37291  mapdindp0  37325  hdmaprnlem7N  37464  hdmaprnlem8N  37465  hdmaprnlem3eN  37467  hgmapvvlem3  37534  mzpsubst  37628  eldioph2lem1  37640  eldioph2lem2  37641  eldioph2b  37643  diophin  37653  irrapxlem2  37704  irrapxlem4  37706  irrapxlem5  37707  pellexlem1  37710  pellexlem2  37711  pellexlem6  37715  elpell1qr2  37753  pell1qrgaplem  37754  pell1qrgap  37755  pellqrex  37760  pellfundex  37767  pellfund14  37779  rmspecsqrtnq  37787  rmspecsqrtnqOLD  37788  rmxyadd  37803  expmordi  37829  rmxypos  37831  jm2.24  37847  congsub  37854  mzpcong  37856  congrep  37857  acongtr  37862  acongrep  37864  jm2.19lem1  37873  jm2.22  37879  jm2.23  37880  jm2.26lem3  37885  jm2.26  37886  jm2.27a  37889  fnwe2lem2  37938  aomclem6  37946  hbtlem2  38011  hbtlem4  38013  hbtlem5  38015  dgraa0p  38036  rngunsnply  38060  acsfn1p  38086  proot1hash  38095  itgpowd  38117  expgrowth  38851  fpmd  39797  abslt2sqd  39889  ioondisj2  40032  ioondisj1  40033  eliocre  40052  ioossioobi  40061  iooiinicc  40087  iooiinioc  40101  icossico2  40109  lptioo2  40181  limcresiooub  40192  limsupequzlem  40272  xlimmnfvlem2  40377  xlimpnfvlem2  40381  cncfuni  40417  cncfiooicclem1  40424  cxpcncf2  40431  dvcnre  40448  dvresntr  40450  dvmptresicc  40452  dvresioo  40454  dvbdfbdioolem1  40461  dvnmptdivc  40471  dvnxpaek  40475  itgsinexplem1  40487  itgcoscmulx  40503  itgiccshift  40514  itgperiod  40515  ovolsplit  40523  stoweidlem11  40546  stoweidlem26  40561  stoweidlem34  40569  stoweidlem36  40571  stoweidlem38  40573  stirlinglem5  40613  dirkercncflem2  40639  dirkercncflem4  40641  fourierdlem20  40662  fourierdlem58  40699  fourierdlem72  40713  fourierdlem73  40714  fourierdlem74  40715  fourierdlem75  40716  fourierdlem76  40717  fourierdlem79  40720  fourierdlem80  40721  fourierdlem87  40728  fourierdlem94  40735  fourierdlem103  40744  fourierdlem104  40745  fourierdlem107  40748  fourierdlem113  40754  sqwvfoura  40763  sqwvfourb  40764  fourierswlem  40765  fouriersw  40766  etransclem46  40815  etransclem47  40816  rrndistlt  40828  rrnprjdstle  40839  ioorrnopnxrlem  40844  sge0ssre  40932  sge0seq  40981  hsphoidmvle2  41120  hsphoidmvle  41121  hoidmv1lelem1  41126  hoidmv1lelem2  41127  hoidmv1lelem3  41128  hoidmvlelem1  41130  hoidifhspdmvle  41155  hoiqssbllem2  41158  ovolval5lem2  41188  iinhoiicc  41209  iunhoiioo  41211  vonioolem2  41216  vonicclem2  41219  issmflem  41257  iccpartdisj  41698  m1expevenALTV  41885  oexpnegALTV  41913  tgoldbach  42030  tgoldbachOLD  42037  nn0eo  42647  fdivpm  42662  refdivpm  42663  elbigolo1  42676  logbpw2m1  42686  fllog2  42687  dignn0flhalflem1  42734  dignn0flhalflem2  42735
  Copyright terms: Public domain W3C validator