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

Theorem syl22anc 858
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 503 . 2 (𝜑 → (𝜓𝜒))
4 syl12anc.3 . 2 (𝜑𝜃)
5 syl22anc.4 . 2 (𝜑𝜏)
6 syl22anc.5 . 2 (((𝜓𝜒) ∧ (𝜃𝜏)) → 𝜂)
73, 4, 5, 6syl12anc 856 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:  preqsnd  4586  preqsndOLD  4587  fr2nr  5296  soltmin  5750  f1oprg  6400  f1prex  6766  fveqf1o  6784  weniso  6831  fr3nr  7212  smogt  7703  smorndom  7704  oacomf1o  7885  difsnen  8284  undom  8290  enfixsn  8311  domss2  8361  ssenen  8376  marypha1lem  8581  fisupcl  8617  ordtypelem3  8667  ordtypelem8  8672  oieu  8686  oismo  8687  wofib  8692  wemaplem2  8694  wemapso  8698  wemapso2lem  8699  unxpwdom2  8735  infdifsn  8804  oemapvali  8831  cantnflem1c  8834  cantnflem1  8836  cantnf  8840  cnfcom3  8851  r1ordg  8891  dif1card  9119  infxpenlem  9122  dfac8clem  9141  infxp  9325  infmap2  9328  cflim2  9373  coftr  9383  fin2i2  9428  enfin2i  9431  fin23lem26  9435  fin23lem27  9438  fin23lem40  9461  isf32lem2  9464  isf32lem3  9465  isf32lem4  9466  isf32lem7  9469  isf32lem9  9471  fin1a2lem13  9522  fin12  9523  alephexp1  9689  gchdomtri  9739  fpwwe2lem12  9751  fpwwe2lem13  9752  gchpwdom  9780  gchhar  9789  adderpqlem  10064  mulerpqlem  10065  addassnq  10068  mulassnq  10069  distrnq  10071  mulidnq  10073  recmulnq  10074  ltexnq  10085  distrlem1pr  10135  distrlem4pr  10136  prlem936  10157  reclem3pr  10159  mulcmpblnr  10180  mulgt0d  10480  mul4d  10536  add4d  10552  add42d  10553  subcan  10624  addsub4d  10727  subadd4d  10728  sub4d  10729  2addsubd  10730  addsubeq4d  10731  muladdd  10777  mulsubd  10778  addgegt0d  10889  addge0d  10891  mulge0d  10892  le2addd  10934  le2subd  10935  ltleaddd  10936  leltaddd  10937  lt2subd  10939  divdivdiv  11014  divcan5  11015  divne0d  11105  recdivd  11106  recdiv2d  11107  divcan6d  11108  ddcand  11109  rec11d  11110  divmuldivd  11130  divmul13d  11131  divmul24d  11132  divadddivd  11133  divsubdivd  11134  divmuleqd  11135  divdivdivd  11136  subrecd  11144  mulge0b  11181  recreclt  11210  divgt0d  11247  mulgt1d  11248  lemulge11d  11249  lemulge12d  11250  ltmul12ad  11253  lemul12ad  11254  lemul12bd  11255  supmul1  11280  nndivtr  11351  qreccl  12030  ledivdivd  12114  lediv12ad  12148  lt2mul2divd  12158  xlt2add  12311  supxrun  12367  supxrre  12378  infxrre  12387  elicore  12447  iccss2  12465  iccssico2  12468  lincmb01cmp  12541  iccf1o  12542  fzrev2i  12631  fz1fzo0m1  12743  2tnp1ge0ge0  12857  m1modnnsub1  12943  modaddmodup  12960  modaddmodlo  12961  modsubdir  12966  fzennn  12994  sermono  13059  mulexpz  13126  expaddz  13130  ltexp2a  13138  leexp2a  13142  sqdiv  13154  expmulnbnd  13222  digit1  13224  expsubd  13245  lt2sqd  13269  le2sqd  13270  sq11d  13271  bcm1k  13325  bcp1n  13326  bcp1nk  13327  hashf1lem1  13459  cshw1  13795  2swrd2eqwrdeq  13924  ofccat  13936  absrele  14274  sqreulem  14325  sqrtmuld  14389  sqrtsq2d  14390  sqrtled  14391  sqrtltd  14392  sqr11d  14393  abs3lemd  14426  rlimuni  14507  climuni  14509  lo1resb  14521  o1resb  14523  2clim  14529  addcn2  14550  mulcn2  14552  o1of2  14569  o1rlimmul  14575  lo1add  14583  lo1mul  14584  isercolllem1  14621  caucvgrlem  14629  iseraltlem2  14639  iseraltlem3  14640  mptfzshft  14735  fsumrev  14736  fsum0diag2  14740  binomlem  14786  climcndslem1  14806  climcndslem2  14807  harmonic  14816  mertenslem1  14840  fprodser  14903  fprodrev  14931  rprisefaccl  14977  efcllem  15031  moddvds  15217  dvds1  15267  dvdsext  15269  evennn2n  15298  bitsinv1  15386  sadaddlem  15410  sadasslem  15414  sadeq  15416  mulgcd  15487  dvdssqlem  15501  lcmftp  15571  rpmulgcd2  15591  coprmproddvdslem  15597  isprm5  15639  isprm6  15646  crth  15703  eulerthlem2  15707  prmdiveq  15711  pythagtriplem11  15750  pythagtriplem13  15752  pcgcd1  15801  pcprmpw2  15806  pcaddlem  15812  fldivp1  15821  4sqlem12  15880  4sqlem14  15882  4sqlem15  15883  4sqlem16  15884  vdwapun  15898  mreexexlem4d  16515  acsfn1  16529  acsfn2  16531  sscpwex  16682  rescabs  16700  yonedainv  17129  subm0  17564  pmtrfb  18089  psgnunilem1  18117  odmodnn0  18163  odeq  18173  dfod2  18185  sylow1lem1  18217  lsmsubg  18273  lsmmod  18292  lsmdisj2  18299  ghmplusg  18453  odadd  18457  gexexlem  18459  lt6abl  18500  cyggex2  18502  dprdfinv  18623  dmdprdsplitlem  18641  dpjidcl  18662  ablfacrp  18670  ablfacrp2  18671  ablfac1c  18675  ablfac1eu  18677  lcomfsupp  19110  lssvancl1  19152  lssvnegcl  19166  lspprvacl  19209  lspsneli  19211  lspsn  19212  lmhmplusg  19254  lmhmima  19257  lmhmpreima  19258  reslmhm  19262  lbsind2  19291  lsmcl  19293  lsmelval2  19295  lsppreli  19300  lspprabs  19305  pj1lmhm  19310  lssvs0or  19320  lspabs3  19331  lspfixed  19338  lspfixedOLD  19339  lspexch  19340  lsmcv  19352  lspsolv  19354  lidlmcl  19429  drngnidl  19441  2idlcpbl  19446  mplbas2  19682  evlslem3  19725  evlslem1  19726  coe1addfv  19846  lply1binom  19887  evl1addd  19916  evl1subd  19917  evl1muld  19918  gzrngunit  20023  zringlpirlem3  20045  prmirredlem  20052  znf1o  20110  znunithash  20123  frlmsubgval  20322  frlmvscaval  20324  frlmphllem  20333  frlmphl  20334  frlmssuvc1  20347  frlmsslsp  20349  frlmup1  20351  frlmup2  20352  lindfind2  20371  lindfrn  20374  f1lindf  20375  islindf4  20391  mamudi  20423  mamudir  20424  1marepvmarrepid  20596  mdetrlin  20623  smadiadetglem1  20693  smadiadetg  20695  cramerimplem1  20705  cramerimplem1OLD  20706  mat2pmatscmxcl  20762  m2pmfzgsumcl  20770  pmatcollpw  20803  pmatcollpwfi  20804  pmatcollpw3fi1lem1  20808  cpmidpmatlem2  20893  cpmadugsumlemF  20898  chcoeffeqlem  20907  ntrin  21083  topssnei  21146  restbas  21180  restntr  21204  cnntri  21293  fiuncmp  21425  nllyrest  21507  nllyidm  21510  hausllycmp  21515  cldllycmp  21516  hauspwdom  21522  txcld  21624  txcn  21647  txlly  21657  txnlly  21658  txhaus  21668  txlm  21669  txkgen  21673  xkococnlem  21680  cnmpt2res  21698  xkoinjcn  21708  basqtop  21732  qtopeu  21737  trfbas2  21864  neifil  21901  hausflim  22002  alexsubALTlem2  22069  cnextfval  22083  cnextfvval  22086  cnextf  22087  cnextfres  22090  clssubg  22129  utop2nei  22271  utop3cls  22272  utopreg  22273  psmetlecl  22337  xmetlecl  22368  prdsxmetlem  22390  bldisj  22420  imasf1obl  22510  prdsbl  22513  stdbdmet  22538  stdbdmopn  22540  met2ndci  22544  metcnp  22563  metustto  22575  metustexhalf  22578  cfilucfil  22581  metucn  22593  lssnlm  22722  nmotri  22760  nmoid  22763  tgioo  22816  blcvx  22818  xrsmopn  22832  reperflem  22838  reconnlem2  22847  opnreen  22851  metdsge  22869  metdsre  22873  metdscnlem  22875  metnrmlem1a  22878  metnrmlem1  22879  metnrmlem3  22881  cncfmet  22928  cnmpt2pc  22944  icopnfcnv  22958  icopnfhmeo  22959  cnllycmp  22972  evth  22975  lebnumii  22982  nmoleub2lem3  23131  iscfil2  23281  cfil3i  23284  iscfil3  23288  cfilfcls  23289  iscau3  23293  iscmet3lem2  23307  caubl  23323  lmcau  23328  rrxcph  23398  minveclem2  23415  pjthlem1  23426  pjthlem2  23427  ivthicc  23445  ovollecl  23470  ovolunlem1a  23483  ovolunnul  23487  ovoliunlem1  23489  ismbl2  23514  nulmbl2  23523  unmbl  23524  volun  23532  voliunlem2  23538  ioombl1lem2  23546  uniioombllem2a  23569  uniioombllem3  23572  uniioombllem4  23573  dyaddisjlem  23582  dyadmaxlem  23584  opnmbllem  23588  volsup2  23592  volcn  23593  ismbfd  23626  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  24618  efopn  24624  logtayllem  24625  logccv  24629  cxplt3  24666  cxpmul2zd  24682  cxpltd  24685  cxpled  24686  cxplt3d  24698  cxple3d  24699  dvsqrt  24703  cxpcn3  24709  cxpaddle  24713  cxpeq  24718  angcan  24752  angvald  24754  ang180lem2  24760  ang180  24764  isosctrlem3  24770  dquartlem1  24798  atantayl2  24885  leibpilem1  24887  leibpi  24889  log2tlbnd  24892  birthdaylem3  24900  xrlimcnp  24915  efrlim  24916  o1cxp  24921  jensenlem2  24934  jensen  24935  fsumharmonic  24958  lgamucov  24984  lgamcvg2  25001  wilthlem1  25014  basellem3  25029  basellem6  25032  basellem8  25034  ppisval  25050  chtwordi  25102  ppiwordi  25108  mumullem2  25126  dvdsmulf1o  25140  fsumvma  25158  fsumvma2  25159  chpchtsum  25164  chpub  25165  logfacubnd  25166  dchrmulcl  25194  dchrinv  25206  dchrptlem1  25209  dchrptlem2  25210  sumdchr2  25215  dchr2sum  25218  bposlem7  25235  lgslem1  25242  lgslem3  25244  lgsdirprm  25276  lgsqrlem2  25292  lgseisenlem1  25320  lgseisenlem2  25321  lgseisenlem4  25323  lgseisen  25324  lgsquadlem1  25325  lgsquad2lem1  25329  lgsquad3  25332  m1lgs  25333  2sqlem7  25369  chebbnd1lem2  25379  chebbnd1lem3  25380  rplogsumlem1  25393  rpvmasumlem  25396  dchrvmasumlem1  25404  dchrvmasum2lem  25405  dchrvmasumlema  25409  dchrisum0flblem2  25418  dchrisum0fno1  25420  dchrisum0re  25422  logdivsum  25442  pntrsumbnd2  25476  pntpbnd1a  25494  pntpbnd1  25495  pntibndlem2  25500  pntlemr  25511  pntlemj  25512  pntlemf  25514  pnt2  25522  padicabv  25539  ostth2lem2  25543  f1otrg  25971  brbtwn2  26005  colinearalglem2  26007  axcgrtr  26015  axcgrid  26016  axsegconlem7  26023  axsegcon  26027  ax5seglem3  26031  ax5seglem6  26034  ax5seg  26038  axpaschlem  26040  axlowdimlem17  26058  axcontlem2  26065  axcontlem4  26067  axcontlem7  26070  axcontlem8  26071  ecgrtg  26083  usgredg2v  26340  vtxdgoddnumeven  26683  2trlond  27085  clwwlknonex2  27284  eupthp1  27395  nmobndi  27964  ubthlem2  28061  ubthlem3  28062  minvecolem2  28065  shuni  28493  pjhthlem1  28584  chscllem2  28831  pjcompi  28865  mayete3i  28921  unoplin  29113  hmoplin  29135  nmophmi  29224  mdslmd4i  29526  isoun  29812  xrge0addcld  29860  xrofsup  29866  eliccelico  29872  elicoelioo  29873  difioo  29877  rexdiv  29965  2sqmod  29979  xrge0addgt0  30022  omndadd2d  30039  omndadd2rd  30040  omndmul2  30043  ofldchr  30145  mdetpmtr2  30221  mdetpmtr12  30222  madjusmdetlem1  30224  madjusmdetlem4  30227  unitdivcld  30278  xrge0mulc1cn  30318  qqhnm  30365  esumcst  30456  esumfsup  30463  esumpmono  30472  esumcvg  30479  difelsiga  30527  sigapisys  30549  sigapildsys  30556  ldgenpisyslem1  30557  1stmbfm  30653  2ndmbfm  30654  dya2icoseg  30670  sibfinima  30732  probmeasb  30823  orvcgteel  30860  orvclteel  30865  ballotlemsima  30908  ballotlemfrceq  30921  sgnmul  30935  ccatmulgnn0dir  30950  fct2relem  31006  ftc2re  31007  chtvalz  31038  subfacp1lem2a  31490  subfaclim  31498  erdsze2lem2  31514  cvmliftlem2  31596  cvmliftlem10  31604  cvmliftlem13  31606  cvmliftiota  31611  cvmlift2lem9  31621  cvmlift2lem11  31623  cvmlift2lem12  31624  cvmliftphtlem  31627  cvmlift3lem6  31634  cvmlift3lem7  31635  cvmlift3lem9  31637  snmlff  31639  mrsubfval  31733  trpredelss  32057  trpredpo  32060  wzel  32095  wsuclem  32096  sltrec  32250  brsegle  32541  opnregcld  32651  addgtge0d  32818  fin2so  33711  poimirlem17  33741  poimirlem23  33747  opnmbllem0  33760  mblfinlem3  33763  mblfinlem4  33764  itg2addnclem  33775  itg2addnc  33778  itg2gt0cn  33779  ftc1cnnclem  33797  ftc1cnnc  33798  areacirclem5  33818  indexdom  33843  sstotbnd2  33886  isbnd3  33896  isbnd3b  33897  cntotbnd  33908  ismtyima  33915  heibor1lem  33921  heiborlem8  33930  rrncmslem  33944  reheibor  33951  lkrlsp  34884  lshpkrlem5  34896  ldualssvscl  34940  ldualssvsubcl  34941  llnmlplnN  35321  llncvrlpln  35340  pmapjat1  35635  pclfinN  35682  lautlt  35873  lauteq  35877  lautco  35879  ltrn11  35908  ltrnle  35911  ltrneq2  35930  cdlemednuN  36082  cdleme20k  36101  cdleme20l2  36103  cdleme20l  36104  cdleme20m  36105  cdleme21c  36109  cdleme22e  36126  cdleme22eALTN  36127  cdlemefrs32fva  36182  cdlemg4g  36398  cdlemg18b  36461  cdlemg18c  36462  cdlemj3  36605  dia2dimlem5  36850  dvhopN  36898  cdlemm10N  36900  dihjatcclem4  37203  dochexmidlem2  37243  lclkrlem2o  37303  lcfrlem5  37328  lcfrlem6  37329  lcdlssvscl  37388  mapdpglem6  37460  mapdpglem9  37462  mapdpglem12  37465  mapdpglem14  37467  mapdindp0  37501  hdmaprnlem7N  37637  hdmaprnlem8N  37638  hdmaprnlem3eN  37640  hgmapvvlem3  37707  mzpsubst  37814  eldioph2lem1  37826  eldioph2lem2  37827  eldioph2b  37829  diophin  37839  irrapxlem2  37890  irrapxlem4  37892  irrapxlem5  37893  pellexlem1  37896  pellexlem2  37897  pellexlem6  37901  elpell1qr2  37939  pell1qrgaplem  37940  pell1qrgap  37941  pellqrex  37946  pellfundex  37953  pellfund14  37965  rmspecsqrtnq  37973  rmxyadd  37988  expmordi  38014  rmxypos  38016  jm2.24  38032  congsub  38039  mzpcong  38041  congrep  38042  acongtr  38047  acongrep  38049  jm2.19lem1  38058  jm2.22  38064  jm2.23  38065  jm2.26lem3  38070  jm2.26  38071  jm2.27a  38074  fnwe2lem2  38123  aomclem6  38131  hbtlem2  38196  hbtlem4  38198  hbtlem5  38200  dgraa0p  38221  rngunsnply  38245  acsfn1p  38271  proot1hash  38280  itgpowd  38301  expgrowth  39035  fpmd  39967  abslt2sqd  40057  ioondisj2  40199  ioondisj1  40200  eliocre  40217  ioossioobi  40225  iooiinicc  40250  iooiinioc  40264  icossico2  40272  lptioo2  40344  limcresiooub  40355  limsupequzlem  40435  xlimmnfvlem2  40540  xlimpnfvlem2  40544  cncfuni  40580  cncfiooicclem1  40587  cxpcncf2  40594  dvcnre  40611  dvresntr  40613  dvmptresicc  40615  dvresioo  40617  dvbdfbdioolem1  40624  dvnmptdivc  40634  dvnxpaek  40638  itgsinexplem1  40650  itgcoscmulx  40665  itgiccshift  40676  itgperiod  40677  ovolsplit  40685  stoweidlem11  40708  stoweidlem26  40723  stoweidlem34  40731  stoweidlem36  40733  stoweidlem38  40735  stirlinglem5  40775  dirkercncflem2  40801  dirkercncflem4  40803  fourierdlem20  40824  fourierdlem58  40861  fourierdlem72  40875  fourierdlem73  40876  fourierdlem74  40877  fourierdlem75  40878  fourierdlem76  40879  fourierdlem79  40882  fourierdlem80  40883  fourierdlem87  40890  fourierdlem94  40897  fourierdlem103  40906  fourierdlem104  40907  fourierdlem107  40910  fourierdlem113  40916  sqwvfoura  40925  sqwvfourb  40926  fourierswlem  40927  fouriersw  40928  etransclem46  40977  etransclem47  40978  rrndistlt  40990  rrnprjdstle  41001  ioorrnopnxrlem  41006  sge0ssre  41094  sge0seq  41143  hsphoidmvle2  41282  hsphoidmvle  41283  hoidmv1lelem1  41288  hoidmv1lelem2  41289  hoidmv1lelem3  41290  hoidmvlelem1  41292  hoidifhspdmvle  41317  hoiqssbllem2  41320  ovolval5lem2  41350  iinhoiicc  41371  iunhoiioo  41373  vonioolem2  41378  vonicclem2  41381  issmflem  41419  iccpartdisj  41949  m1expevenALTV  42136  tgoldbach  42281  nn0eo  42891  fdivpm  42906  refdivpm  42907  elbigolo1  42920  logbpw2m1  42930  fllog2  42931  dignn0flhalflem1  42978  dignn0flhalflem2  42979
  Copyright terms: Public domain W3C validator