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

Theorem syl22anc 1477
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 501 . 2 (𝜑 → (𝜓𝜒))
4 syl12anc.3 . 2 (𝜑𝜃)
5 syl22anc.4 . 2 (𝜑𝜏)
6 syl22anc.5 . 2 (((𝜓𝜒) ∧ (𝜃𝜏)) → 𝜂)
73, 4, 5, 6syl12anc 1474 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 197  df-an 383
This theorem is referenced by:  preqsnd  4523  preqsndOLD  4524  fr2nr  5227  soltmin  5673  f1oprg  6322  f1prex  6682  fveqf1o  6700  weniso  6747  fr3nr  7126  smogt  7617  smorndom  7618  oacomf1o  7799  difsnen  8198  undom  8204  enfixsn  8225  domss2  8275  ssenen  8290  marypha1lem  8495  fisupcl  8531  ordtypelem3  8581  ordtypelem8  8586  oieu  8600  oismo  8601  wofib  8606  wemaplem2  8608  wemapso  8612  wemapso2lem  8613  unxpwdom2  8649  infdifsn  8718  oemapvali  8745  cantnflem1c  8748  cantnflem1  8750  cantnf  8754  cnfcom3  8765  r1ordg  8805  dif1card  9033  infxpenlem  9036  dfac8clem  9055  infxp  9239  infmap2  9242  cflim2  9287  coftr  9297  fin2i2  9342  enfin2i  9345  fin23lem26  9349  fin23lem27  9352  fin23lem40  9375  isf32lem2  9378  isf32lem3  9379  isf32lem4  9380  isf32lem7  9383  isf32lem9  9385  fin1a2lem13  9436  fin12  9437  alephexp1  9603  gchdomtri  9653  fpwwe2lem12  9665  fpwwe2lem13  9666  gchpwdom  9694  gchhar  9703  adderpqlem  9978  mulerpqlem  9979  addassnq  9982  mulassnq  9983  distrnq  9985  mulidnq  9987  recmulnq  9988  ltexnq  9999  distrlem1pr  10049  distrlem4pr  10050  prlem936  10071  reclem3pr  10073  mulcmpblnr  10094  mulgt0d  10394  mul4d  10450  add4d  10466  add42d  10467  subcan  10538  addsub4d  10641  subadd4d  10642  sub4d  10643  2addsubd  10644  addsubeq4d  10645  muladdd  10691  mulsubd  10692  addgegt0d  10803  addge0d  10805  mulge0d  10806  le2addd  10848  le2subd  10849  ltleaddd  10850  leltaddd  10851  lt2subd  10853  divdivdiv  10928  divcan5  10929  divne0d  11019  recdivd  11020  recdiv2d  11021  divcan6d  11022  ddcand  11023  rec11d  11024  divmuldivd  11044  divmul13d  11045  divmul24d  11046  divadddivd  11047  divsubdivd  11048  divmuleqd  11049  divdivdivd  11050  subrecd  11058  mulge0b  11095  recreclt  11124  divgt0d  11161  mulgt1d  11162  lemulge11d  11163  lemulge12d  11164  ltmul12ad  11167  lemul12ad  11168  lemul12bd  11169  supmul1  11194  nndivtr  11264  qreccl  12011  ledivdivd  12100  lediv12ad  12134  lt2mul2divd  12144  xlt2add  12295  supxrun  12351  supxrre  12362  infxrre  12371  elicore  12431  iccss2  12449  iccssico2  12452  lincmb01cmp  12522  iccf1o  12523  fzrev2i  12612  fz1fzo0m1  12724  2tnp1ge0ge0  12838  m1modnnsub1  12924  modaddmodup  12941  modaddmodlo  12942  modsubdir  12947  fzennn  12975  sermono  13040  mulexpz  13107  expaddz  13111  ltexp2a  13119  leexp2a  13123  sqdiv  13135  expmulnbnd  13203  digit1  13205  expsubd  13226  lt2sqd  13250  le2sqd  13251  sq11d  13252  bcm1k  13306  bcp1n  13307  bcp1nk  13308  hashf1lem1  13441  cshw1  13777  2swrd2eqwrdeq  13906  ofccat  13918  absrele  14256  sqreulem  14307  sqrtmuld  14371  sqrtsq2d  14372  sqrtled  14373  sqrtltd  14374  sqr11d  14375  abs3lemd  14408  rlimuni  14489  climuni  14491  lo1resb  14503  o1resb  14505  2clim  14511  addcn2  14532  mulcn2  14534  o1of2  14551  o1rlimmul  14557  lo1add  14565  lo1mul  14566  isercolllem1  14603  caucvgrlem  14611  iseraltlem2  14621  iseraltlem3  14622  mptfzshft  14717  fsumrev  14718  fsum0diag2  14722  binomlem  14768  climcndslem1  14788  climcndslem2  14789  harmonic  14798  mertenslem1  14823  fprodser  14886  fprodrev  14914  rprisefaccl  14960  efcllem  15014  moddvds  15200  dvds1  15250  dvdsext  15252  evennn2n  15283  bitsinv1  15372  sadaddlem  15396  sadasslem  15400  sadeq  15402  mulgcd  15473  dvdssqlem  15487  lcmftp  15557  rpmulgcd2  15577  coprmproddvdslem  15583  isprm5  15626  isprm6  15633  crth  15690  eulerthlem2  15694  prmdiveq  15698  pythagtriplem11  15737  pythagtriplem13  15739  pcgcd1  15788  pcprmpw2  15793  pcaddlem  15799  fldivp1  15808  4sqlem12  15867  4sqlem14  15869  4sqlem15  15870  4sqlem16  15871  vdwapun  15885  mreexexlem4d  16515  acsfn1  16529  acsfn2  16531  sscpwex  16682  rescabs  16700  yonedainv  17129  subm0  17564  pmtrfb  18092  psgnunilem1  18120  odmodnn0  18166  odeq  18176  dfod2  18188  sylow1lem1  18220  lsmsubg  18276  lsmmod  18295  lsmdisj2  18302  ghmplusg  18456  odadd  18460  gexexlem  18462  lt6abl  18503  cyggex2  18505  dprdfinv  18626  dmdprdsplitlem  18644  dpjidcl  18665  ablfacrp  18673  ablfacrp2  18674  ablfac1c  18678  ablfac1eu  18680  lcomfsupp  19113  lssvancl1  19155  lssvnegcl  19169  lspprvacl  19212  lspsneli  19214  lspsn  19215  lmhmplusg  19257  lmhmima  19260  lmhmpreima  19261  reslmhm  19265  lbsind2  19294  lsmcl  19296  lsmelval2  19298  lsppreli  19303  lspprabs  19308  pj1lmhm  19313  lssvs0or  19323  lspabs3  19334  lspfixed  19341  lspfixedOLD  19342  lspexch  19343  lsmcv  19355  lspsolv  19357  lidlmcl  19432  drngnidl  19444  2idlcpbl  19449  mplbas2  19685  evlslem3  19729  evlslem1  19730  coe1addfv  19850  lply1binom  19891  evl1addd  19920  evl1subd  19921  evl1muld  19922  gzrngunit  20027  zringlpirlem3  20049  prmirredlem  20056  znf1o  20115  znunithash  20128  frlmsubgval  20325  frlmvscaval  20327  frlmphllem  20336  frlmphl  20337  frlmssuvc1  20350  frlmsslsp  20352  frlmup1  20354  frlmup2  20355  lindfind2  20374  lindfrn  20377  f1lindf  20378  islindf4  20394  mamudi  20426  mamudir  20427  1marepvmarrepid  20599  mdetrlin  20626  smadiadetglem1  20696  smadiadetg  20698  cramerimplem1  20708  cramerimplem1OLD  20709  mat2pmatscmxcl  20765  m2pmfzgsumcl  20773  pmatcollpw  20806  pmatcollpwfi  20807  pmatcollpw3fi1lem1  20811  cpmidpmatlem2  20896  cpmadugsumlemF  20901  chcoeffeqlem  20910  ntrin  21086  topssnei  21149  restbas  21183  restntr  21207  cnntri  21296  fiuncmp  21428  nllyrest  21510  nllyidm  21513  hausllycmp  21518  cldllycmp  21519  hauspwdom  21525  txcld  21627  txcn  21650  txlly  21660  txnlly  21661  txhaus  21671  txlm  21672  txkgen  21676  xkococnlem  21683  cnmpt2res  21701  xkoinjcn  21711  basqtop  21735  qtopeu  21740  trfbas2  21867  neifil  21904  hausflim  22005  alexsubALTlem2  22072  cnextfval  22086  cnextfvval  22089  cnextf  22090  cnextfres  22093  clssubg  22132  utop2nei  22274  utop3cls  22275  utopreg  22276  psmetlecl  22340  xmetlecl  22371  prdsxmetlem  22393  bldisj  22423  imasf1obl  22513  prdsbl  22516  stdbdmet  22541  stdbdmopn  22543  met2ndci  22547  metcnp  22566  metustto  22578  metustexhalf  22581  cfilucfil  22584  metucn  22596  lssnlm  22725  nmotri  22763  nmoid  22766  tgioo  22819  blcvx  22821  xrsmopn  22835  reperflem  22841  reconnlem2  22850  opnreen  22854  metdsge  22872  metdsre  22876  metdscnlem  22878  metnrmlem1a  22881  metnrmlem1  22882  metnrmlem3  22884  cncfmet  22931  cnmpt2pc  22947  icopnfcnv  22961  icopnfhmeo  22962  cnllycmp  22975  evth  22978  lebnumii  22985  nmoleub2lem3  23134  iscfil2  23283  cfil3i  23286  iscfil3  23290  cfilfcls  23291  iscau3  23295  iscmet3lem2  23309  caubl  23325  lmcau  23330  rrxcph  23399  minveclem2  23416  pjthlem1  23427  pjthlem2  23428  ivthicc  23446  ovollecl  23471  ovolunlem1a  23484  ovolunnul  23488  ovoliunlem1  23490  ismbl2  23515  nulmbl2  23524  unmbl  23525  volun  23533  voliunlem2  23539  ioombl1lem2  23547  uniioombllem2a  23570  uniioombllem3  23573  uniioombllem4  23574  dyaddisjlem  23583  dyadmaxlem  23585  opnmbllem  23589  volsup2  23593  volcn  23594  ismbfd  23627  mbfi1fseqlem1  23702  mbfi1fseqlem5  23706  itg2lecl  23725  itg2monolem2  23738  itg2gt0  23747  itgspliticc  23823  ellimc3  23863  limcres  23870  dvfval  23881  dvres3  23897  dvres3a  23898  dvnff  23906  dvnadd  23912  dvn2bss  23913  dvnres  23914  dvcmul  23927  dvcmulf  23928  dvmptres3  23939  dvmptres2  23945  dvmptntr  23954  dvexp3  23961  dvferm1lem  23967  dvlip  23976  dvlipcn  23977  dvlip2  23978  c1liplem1  23979  dvgt0lem1  23985  dvgt0lem2  23986  dvne0  23994  lhop1lem  23996  lhop2  23998  lhop  23999  dvcnvrelem1  24000  dvcnvrelem2  24001  dvcvx  24003  dvfsumle  24004  dvfsumabs  24006  dvfsumlem2  24010  ftc1lem6  24024  ftc1  24025  ftc2ditglem  24028  itgsubstlem  24031  tdeglem4  24040  mdegaddle  24054  mdegmullem  24058  ply1rem  24143  fta1glem2  24146  fta1blem  24148  ig1peu  24151  ig1pdvds  24156  dgrmulc  24247  dgrcolem1  24249  plydivlem4  24271  plydiveu  24273  fta1lem  24282  vieta1lem1  24285  vieta1lem2  24286  plyexmo  24288  taylfvallem1  24331  taylfval  24333  tayl0  24336  taylplem1  24337  taylply2  24342  taylply  24343  dvtaylp  24344  dvntaylp  24345  dvntaylp0  24346  taylthlem1  24347  taylthlem2  24348  ulmcaulem  24368  ulmcau  24369  ulmcn  24373  ulmdvlem1  24374  radcnvlem1  24387  radcnvle  24394  psercn  24400  pserdvlem2  24402  pserdv  24403  abelth  24415  cosordlem  24498  tanregt0  24506  dvlog2lem  24619  efopn  24625  logtayllem  24626  logccv  24630  cxplt3  24667  cxpmul2zd  24683  cxpltd  24686  cxpled  24687  cxplt3d  24699  cxple3d  24700  dvsqrt  24704  cxpcn3  24710  cxpaddle  24714  cxpeq  24719  angcan  24753  angvald  24755  ang180lem2  24761  ang180  24765  isosctrlem3  24771  dquartlem1  24799  atantayl2  24886  leibpilem1  24888  leibpi  24890  log2tlbnd  24893  birthdaylem3  24901  xrlimcnp  24916  efrlim  24917  o1cxp  24922  jensenlem2  24935  jensen  24936  fsumharmonic  24959  lgamucov  24985  lgamcvg2  25002  wilthlem1  25015  basellem3  25030  basellem6  25033  basellem8  25035  ppisval  25051  chtwordi  25103  ppiwordi  25109  mumullem2  25127  dvdsmulf1o  25141  fsumvma  25159  fsumvma2  25160  chpchtsum  25165  chpub  25166  logfacubnd  25167  dchrmulcl  25195  dchrinv  25207  dchrptlem1  25210  dchrptlem2  25211  sumdchr2  25216  dchr2sum  25219  bposlem7  25236  lgslem1  25243  lgslem3  25245  lgsdirprm  25277  lgsqrlem2  25293  lgseisenlem1  25321  lgseisenlem2  25322  lgseisenlem4  25324  lgseisen  25325  lgsquadlem1  25326  lgsquad2lem1  25330  lgsquad3  25333  m1lgs  25334  2sqlem7  25370  chebbnd1lem2  25380  chebbnd1lem3  25381  rplogsumlem1  25394  rpvmasumlem  25397  dchrvmasumlem1  25405  dchrvmasum2lem  25406  dchrvmasumlema  25410  dchrisum0flblem2  25419  dchrisum0fno1  25421  dchrisum0re  25423  logdivsum  25443  pntrsumbnd2  25477  pntpbnd1a  25495  pntpbnd1  25496  pntibndlem2  25501  pntlemr  25512  pntlemj  25513  pntlemf  25515  pnt2  25523  padicabv  25540  ostth2lem2  25544  f1otrg  25972  brbtwn2  26006  colinearalglem2  26008  axcgrtr  26016  axcgrid  26017  axsegconlem7  26024  axsegcon  26028  ax5seglem3  26032  ax5seglem6  26035  ax5seg  26039  axpaschlem  26041  axlowdimlem17  26059  axcontlem2  26066  axcontlem4  26068  axcontlem7  26071  axcontlem8  26072  ecgrtg  26084  usgredg2v  26341  vtxdgoddnumeven  26684  2trlond  27086  clwwlknonex2  27285  eupthp1  27396  nmobndi  27970  ubthlem2  28067  ubthlem3  28068  minvecolem2  28071  shuni  28499  pjhthlem1  28590  chscllem2  28837  pjcompi  28871  mayete3i  28927  unoplin  29119  hmoplin  29141  nmophmi  29230  mdslmd4i  29532  isoun  29819  xrge0addcld  29867  xrofsup  29873  eliccelico  29879  elicoelioo  29880  difioo  29884  rexdiv  29974  2sqmod  29988  xrge0addgt0  30031  omndadd2d  30048  omndadd2rd  30049  omndmul2  30052  ofldchr  30154  mdetpmtr2  30230  mdetpmtr12  30231  madjusmdetlem1  30233  madjusmdetlem4  30236  unitdivcld  30287  xrge0mulc1cn  30327  qqhnm  30374  esumcst  30465  esumfsup  30472  esumpmono  30481  esumcvg  30488  difelsiga  30536  sigapisys  30558  sigapildsys  30565  ldgenpisyslem1  30566  1stmbfm  30662  2ndmbfm  30663  dya2icoseg  30679  sibfinima  30741  probmeasb  30832  orvcgteel  30869  orvclteel  30874  ballotlemsima  30917  ballotlemfrceq  30930  sgnmul  30944  ccatmulgnn0dir  30959  fct2relem  31015  ftc2re  31016  chtvalz  31047  subfacp1lem2a  31500  subfaclim  31508  erdsze2lem2  31524  cvmliftlem2  31606  cvmliftlem10  31614  cvmliftlem13  31616  cvmliftiota  31621  cvmlift2lem9  31631  cvmlift2lem11  31633  cvmlift2lem12  31634  cvmliftphtlem  31637  cvmlift3lem6  31644  cvmlift3lem7  31645  cvmlift3lem9  31647  snmlff  31649  mrsubfval  31743  trpredelss  32068  trpredpo  32071  wzel  32106  wsuclem  32107  sltrec  32261  brsegle  32552  opnregcld  32662  addgtge0d  32833  fin2so  33729  poimirlem17  33759  poimirlem23  33765  opnmbllem0  33778  mblfinlem3  33781  mblfinlem4  33782  itg2addnclem  33793  itg2addnc  33796  itg2gt0cn  33797  ftc1cnnclem  33815  ftc1cnnc  33816  areacirclem5  33836  indexdom  33861  sstotbnd2  33905  isbnd3  33915  isbnd3b  33916  cntotbnd  33927  ismtyima  33934  heibor1lem  33940  heiborlem8  33949  rrncmslem  33963  reheibor  33970  lkrlsp  34911  lshpkrlem5  34923  ldualssvscl  34967  ldualssvsubcl  34968  llnmlplnN  35347  llncvrlpln  35366  pmapjat1  35661  pclfinN  35708  lautlt  35899  lauteq  35903  lautco  35905  ltrn11  35934  ltrnle  35937  ltrneq2  35956  cdlemednuN  36109  cdleme20k  36128  cdleme20l2  36130  cdleme20l  36131  cdleme20m  36132  cdleme21c  36136  cdleme22e  36153  cdleme22eALTN  36154  cdlemefrs32fva  36209  cdlemg4g  36425  cdlemg18b  36488  cdlemg18c  36489  cdlemj3  36632  dia2dimlem5  36878  dvhopN  36926  cdlemm10N  36928  dihjatcclem4  37231  dochexmidlem2  37271  lclkrlem2o  37331  lcfrlem5  37356  lcfrlem6  37357  lcdlssvscl  37416  mapdpglem6  37488  mapdpglem9  37490  mapdpglem12  37493  mapdpglem14  37495  mapdindp0  37529  hdmaprnlem7N  37665  hdmaprnlem8N  37666  hdmaprnlem3eN  37668  hgmapvvlem3  37735  mzpsubst  37837  eldioph2lem1  37849  eldioph2lem2  37850  eldioph2b  37852  diophin  37862  irrapxlem2  37913  irrapxlem4  37915  irrapxlem5  37916  pellexlem1  37919  pellexlem2  37920  pellexlem6  37924  elpell1qr2  37962  pell1qrgaplem  37963  pell1qrgap  37964  pellqrex  37969  pellfundex  37976  pellfund14  37988  rmspecsqrtnq  37996  rmspecsqrtnqOLD  37997  rmxyadd  38012  expmordi  38038  rmxypos  38040  jm2.24  38056  congsub  38063  mzpcong  38065  congrep  38066  acongtr  38071  acongrep  38073  jm2.19lem1  38082  jm2.22  38088  jm2.23  38089  jm2.26lem3  38094  jm2.26  38095  jm2.27a  38098  fnwe2lem2  38147  aomclem6  38155  hbtlem2  38220  hbtlem4  38222  hbtlem5  38224  dgraa0p  38245  rngunsnply  38269  acsfn1p  38295  proot1hash  38304  itgpowd  38326  expgrowth  39060  fpmd  40001  abslt2sqd  40092  ioondisj2  40235  ioondisj1  40236  eliocre  40254  ioossioobi  40262  iooiinicc  40287  iooiinioc  40301  icossico2  40309  lptioo2  40381  limcresiooub  40392  limsupequzlem  40472  xlimmnfvlem2  40577  xlimpnfvlem2  40581  cncfuni  40617  cncfiooicclem1  40624  cxpcncf2  40631  dvcnre  40648  dvresntr  40650  dvmptresicc  40652  dvresioo  40654  dvbdfbdioolem1  40661  dvnmptdivc  40671  dvnxpaek  40675  itgsinexplem1  40687  itgcoscmulx  40702  itgiccshift  40713  itgperiod  40714  ovolsplit  40722  stoweidlem11  40745  stoweidlem26  40760  stoweidlem34  40768  stoweidlem36  40770  stoweidlem38  40772  stirlinglem5  40812  dirkercncflem2  40838  dirkercncflem4  40840  fourierdlem20  40861  fourierdlem58  40898  fourierdlem72  40912  fourierdlem73  40913  fourierdlem74  40914  fourierdlem75  40915  fourierdlem76  40916  fourierdlem79  40919  fourierdlem80  40920  fourierdlem87  40927  fourierdlem94  40934  fourierdlem103  40943  fourierdlem104  40944  fourierdlem107  40947  fourierdlem113  40953  sqwvfoura  40962  sqwvfourb  40963  fourierswlem  40964  fouriersw  40965  etransclem46  41014  etransclem47  41015  rrndistlt  41027  rrnprjdstle  41038  ioorrnopnxrlem  41043  sge0ssre  41131  sge0seq  41180  hsphoidmvle2  41319  hsphoidmvle  41320  hoidmv1lelem1  41325  hoidmv1lelem2  41326  hoidmv1lelem3  41327  hoidmvlelem1  41329  hoidifhspdmvle  41354  hoiqssbllem2  41357  ovolval5lem2  41387  iinhoiicc  41408  iunhoiioo  41410  vonioolem2  41415  vonicclem2  41418  issmflem  41456  iccpartdisj  41901  m1expevenALTV  42088  tgoldbach  42233  tgoldbachOLD  42240  nn0eo  42850  fdivpm  42865  refdivpm  42866  elbigolo1  42879  logbpw2m1  42889  fllog2  42890  dignn0flhalflem1  42937  dignn0flhalflem2  42938
  Copyright terms: Public domain W3C validator