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

Theorem syl22anc 834
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 512 . 2 (𝜑 → (𝜓𝜒))
4 syl12anc.3 . 2 (𝜑𝜃)
5 syl22anc.4 . 2 (𝜑𝜏)
6 syl22anc.5 . 2 (((𝜓𝜒) ∧ (𝜃𝜏)) → 𝜂)
73, 4, 5, 6syl12anc 832 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:  preqsnd  4783  fr2nr  5527  soltmin  5990  f1oprg  6653  f1prex  7031  fveqf1o  7049  weniso  7096  fr3nr  7482  suppofssd  7858  smogt  7995  smorndom  7996  oacomf1o  8181  enpr2d  8586  difsnen  8588  undom  8594  enfixsn  8615  domss2  8665  ssenen  8680  marypha1lem  8886  fisupcl  8922  ordtypelem3  8973  ordtypelem8  8978  oieu  8992  oismo  8993  wofib  8998  wemaplem2  9000  wemapso  9004  wemapso2lem  9005  unxpwdom2  9041  infdifsn  9109  oemapvali  9136  cantnflem1c  9139  cantnflem1  9141  cantnf  9145  cnfcom3  9156  r1ordg  9196  dif1card  9425  infxpenlem  9428  dfac8clem  9447  infxp  9626  infmap2  9629  cflim2  9674  coftr  9684  fin2i2  9729  enfin2i  9732  fin23lem26  9736  fin23lem27  9739  fin23lem40  9762  isf32lem2  9765  isf32lem3  9766  isf32lem4  9767  isf32lem7  9770  isf32lem9  9772  fin1a2lem13  9823  fin12  9824  alephexp1  9990  gchdomtri  10040  fpwwe2lem12  10052  fpwwe2lem13  10053  gchpwdom  10081  gchhar  10090  adderpqlem  10365  mulerpqlem  10366  addassnq  10369  mulassnq  10370  distrnq  10372  mulidnq  10374  recmulnq  10375  ltexnq  10386  distrlem1pr  10436  distrlem4pr  10437  prlem936  10458  reclem3pr  10460  mulcmpblnr  10482  mulgt0d  10784  mul4d  10841  add4d  10857  add42d  10858  subcan  10930  addsub4d  11033  subadd4d  11034  sub4d  11035  2addsubd  11036  addsubeq4d  11037  muladdd  11087  mulsubd  11088  addgegt0d  11202  addgtge0d  11203  addge0d  11205  mulge0d  11206  le2addd  11248  le2subd  11249  ltleaddd  11250  leltaddd  11251  lt2subd  11253  divdivdiv  11330  divcan5  11331  divne0d  11421  recdivd  11422  recdiv2d  11423  divcan6d  11424  ddcand  11425  rec11d  11426  divmuldivd  11446  divmul13d  11447  divmul24d  11448  divadddivd  11449  divsubdivd  11450  divmuleqd  11451  divdivdivd  11452  subrecd  11460  mulge0b  11499  recreclt  11528  divgt0d  11564  mulgt1d  11565  lemulge11d  11566  lemulge12d  11567  ltmul12ad  11570  lemul12ad  11571  lemul12bd  11572  supmul1  11599  nndivtr  11673  qreccl  12358  ledivdivd  12446  lediv12ad  12480  lt2mul2divd  12490  xlt2add  12643  supxrun  12699  supxrre  12710  infxrre  12719  elicore  12779  iccss2  12797  iccssico2  12800  lincmb01cmp  12871  iccf1o  12872  fzrev2i  12962  2tnp1ge0ge0  13189  m1modnnsub1  13275  modaddmodup  13292  modaddmodlo  13293  modsubdir  13298  fzennn  13326  sermono  13392  mulexpz  13459  expaddz  13463  sqdiv  13477  expsubd  13511  ltexp2a  13520  expmordi  13521  leexp2a  13526  expmulnbnd  13586  digit1  13588  lt2sqd  13609  le2sqd  13610  sq11d  13611  bcm1k  13665  bcp1n  13666  bcp1nk  13667  hashf1lem1  13803  cshw1  14174  2swrd2eqwrdeq  14305  ofccat  14319  absrele  14658  sqreulem  14709  sqrtmuld  14774  sqrtsq2d  14775  sqrtled  14776  sqrtltd  14777  sqr11d  14778  abs3lemd  14811  rlimuni  14897  climuni  14899  lo1resb  14911  o1resb  14913  2clim  14919  addcn2  14940  mulcn2  14942  o1of2  14959  o1rlimmul  14965  lo1add  14973  lo1mul  14974  isercolllem1  15011  caucvgrlem  15019  iseraltlem2  15029  iseraltlem3  15030  mptfzshft  15123  fsumrev  15124  fsum0diag2  15128  binomlem  15174  climcndslem1  15194  climcndslem2  15195  harmonic  15204  mertenslem1  15230  fprodser  15293  fprodrev  15321  efcllem  15421  moddvds  15608  dvds1  15659  dvdsext  15661  evennn2n  15690  bitsinv1  15781  sadaddlem  15805  sadasslem  15809  sadeq  15811  mulgcd  15886  dvdssqlem  15900  lcmftp  15970  rpmulgcd2  15990  coprmproddvdslem  15996  isprm5  16041  isprm6  16048  crth  16105  eulerthlem2  16109  prmdiveq  16113  pythagtriplem11  16152  pythagtriplem13  16154  pcgcd1  16203  pcprmpw2  16208  pcaddlem  16214  fldivp1  16223  4sqlem12  16282  4sqlem14  16284  4sqlem15  16285  4sqlem16  16286  vdwapun  16300  mreexexlem4d  16908  acsfn1  16922  acsfn2  16924  sscpwex  17075  rescabs  17093  yonedainv  17521  subm0  17970  pmtrfb  18524  psgnunilem1  18552  odmodnn0  18599  odeq  18609  dfod2  18622  sylow1lem1  18654  lsmsubg  18710  lsmmod  18732  lsmdisj2  18739  ghmplusg  18897  odadd  18901  gexexlem  18903  lt6abl  18946  cyggex2  18948  dprdfinv  19072  dmdprdsplitlem  19090  dpjidcl  19111  ablfacrp  19119  ablfacrp2  19120  ablfac1c  19124  ablfac1eu  19126  acsfn1p  19509  lcomfsupp  19605  lssvancl1  19647  lssvnegcl  19659  lspprvacl  19702  lspsneli  19704  lspsn  19705  lmhmplusg  19747  lmhmima  19750  lmhmpreima  19751  reslmhm  19755  lbsind2  19784  lsmcl  19786  lsmelval2  19788  lsppreli  19793  lspprabs  19798  pj1lmhm  19803  lssvs0or  19813  lspabs3  19824  lspfixed  19831  lspexch  19832  lsmcv  19844  lspsolv  19846  lidlmcl  19920  drngnidl  19932  2idlcpbl  19937  mplbas2  20181  evlslem3  20223  evlslem1  20225  coe1addfv  20363  lply1binom  20404  evl1addd  20434  evl1subd  20435  evl1muld  20436  gzrngunit  20541  zringlpirlem3  20563  prmirredlem  20570  znf1o  20628  znunithash  20641  frlmsubgval  20839  frlmvplusgvalc  20841  frlmvscaval  20842  frlmphllem  20854  frlmphl  20855  frlmssuvc1  20868  frlmsslsp  20870  frlmup1  20872  frlmup2  20873  lindfind2  20892  lindfrn  20895  f1lindf  20896  islindf4  20912  mamudi  20942  mamudir  20943  1marepvmarrepid  21114  mdetrlin  21141  smadiadetglem1  21210  smadiadetg  21212  cramerimplem1  21222  mat2pmatscmxcl  21278  m2pmfzgsumcl  21286  pmatcollpw  21319  pmatcollpwfi  21320  pmatcollpw3fi1lem1  21324  cpmidpmatlem2  21409  cpmadugsumlemF  21414  chcoeffeqlem  21423  ntrin  21599  topssnei  21662  restbas  21696  restntr  21720  cnntri  21809  fiuncmp  21942  nllyrest  22024  nllyidm  22027  hausllycmp  22032  cldllycmp  22033  hauspwdom  22039  txcld  22141  txcn  22164  txlly  22174  txnlly  22175  txhaus  22185  txlm  22186  txkgen  22190  xkococnlem  22197  cnmpt2res  22215  xkoinjcn  22225  basqtop  22249  qtopeu  22254  trfbas2  22381  neifil  22418  hausflim  22519  alexsubALTlem2  22586  cnextfval  22600  cnextfvval  22603  cnextf  22604  cnextfres  22607  clssubg  22646  utop2nei  22788  utop3cls  22789  utopreg  22790  psmetlecl  22854  xmetlecl  22885  prdsxmetlem  22907  bldisj  22937  imasf1obl  23027  prdsbl  23030  stdbdmet  23055  stdbdmopn  23057  met2ndci  23061  metcnp  23080  metustto  23092  metustexhalf  23095  cfilucfil  23098  metucn  23110  lssnlm  23239  nmotri  23277  nmoid  23280  tgioo  23333  blcvx  23335  xrsmopn  23349  reperflem  23355  reconnlem2  23364  opnreen  23368  metdsge  23386  metdsre  23390  metdscnlem  23392  metnrmlem1a  23395  metnrmlem1  23396  metnrmlem3  23398  cncfmet  23445  cnmpopc  23461  icopnfcnv  23475  icopnfhmeo  23476  cnllycmp  23489  evth  23492  lebnumii  23499  nmoleub2lem3  23648  iscfil2  23798  cfil3i  23801  iscfil3  23805  cfilfcls  23806  iscau3  23810  iscmet3lem2  23824  caubl  23840  lmcau  23845  cssbn  23907  rrxcph  23924  minveclem2  23958  pjthlem1  23969  pjthlem2  23970  ivthicc  23988  ovollecl  24013  ovolunlem1a  24026  ovolunnul  24030  ovoliunlem1  24032  ismbl2  24057  nulmbl2  24066  unmbl  24067  volun  24075  voliunlem2  24081  ioombl1lem2  24089  uniioombllem2a  24112  uniioombllem3  24115  uniioombllem4  24116  dyaddisjlem  24125  dyadmaxlem  24127  opnmbllem  24131  volsup2  24135  volcn  24136  ismbfd  24169  mbfi1fseqlem1  24245  mbfi1fseqlem5  24249  itg2lecl  24268  itg2monolem2  24281  itg2gt0  24290  itgspliticc  24366  ellimc3  24406  limcres  24413  dvfval  24424  dvres3  24440  dvres3a  24441  dvnff  24449  dvnadd  24455  dvn2bss  24456  dvnres  24457  dvcmul  24470  dvcmulf  24471  dvmptres3  24482  dvmptres2  24488  dvmptntr  24497  dvexp3  24504  dvferm1lem  24510  dvlip  24519  dvlipcn  24520  dvlip2  24521  c1liplem1  24522  dvgt0lem1  24528  dvgt0lem2  24529  dvne0  24537  lhop1lem  24539  lhop2  24541  lhop  24542  dvcnvrelem1  24543  dvcnvrelem2  24544  dvcvx  24546  dvfsumle  24547  dvfsumabs  24549  dvfsumlem2  24553  ftc1lem6  24567  ftc1  24568  ftc2ditglem  24571  itgsubstlem  24574  tdeglem4  24583  mdegaddle  24597  mdegmullem  24601  ply1rem  24686  fta1glem2  24689  fta1blem  24691  ig1peu  24694  ig1pdvds  24699  dgrmulc  24790  dgrcolem1  24792  plydivlem4  24814  plydiveu  24816  fta1lem  24825  vieta1lem1  24828  vieta1lem2  24829  plyexmo  24831  taylfvallem1  24874  taylfval  24876  tayl0  24879  taylplem1  24880  taylply2  24885  taylply  24886  dvtaylp  24887  dvntaylp  24888  dvntaylp0  24889  taylthlem1  24890  taylthlem2  24891  ulmcaulem  24911  ulmcau  24912  ulmcn  24916  ulmdvlem1  24917  radcnvlem1  24930  radcnvle  24937  psercn  24943  pserdvlem2  24945  pserdv  24946  abelth  24958  tanregt0  25050  dvlog2lem  25162  efopn  25168  logtayllem  25169  logccv  25173  cxplt3  25210  cxpmul2zd  25226  cxpltd  25229  cxpled  25230  cxplt3d  25244  cxple3d  25245  dvsqrt  25250  cxpcn3  25256  cxpaddle  25260  cxpeq  25265  angcan  25307  angvald  25309  ang180lem2  25315  ang180  25319  isosctrlem3  25325  dquartlem1  25356  atantayl2  25443  leibpilem1OLD  25446  leibpi  25448  log2tlbnd  25451  birthdaylem3  25459  xrlimcnp  25474  efrlim  25475  o1cxp  25480  jensenlem2  25493  jensen  25494  fsumharmonic  25517  lgamucov  25543  lgamcvg2  25560  wilthlem1  25573  basellem3  25588  basellem6  25591  basellem8  25593  ppisval  25609  chtwordi  25661  ppiwordi  25667  mumullem2  25685  dvdsmulf1o  25699  fsumvma  25717  fsumvma2  25718  chpchtsum  25723  chpub  25724  logfacubnd  25725  dchrmulcl  25753  dchrinv  25765  dchrptlem1  25768  dchrptlem2  25769  sumdchr2  25774  dchr2sum  25777  bposlem7  25794  lgslem1  25801  lgslem3  25803  lgsdirprm  25835  lgsqrlem2  25851  lgseisenlem1  25879  lgseisenlem2  25880  lgseisenlem4  25882  lgseisen  25883  lgsquadlem1  25884  lgsquad2lem1  25888  lgsquad3  25891  m1lgs  25892  2sqlem7  25928  2sq2  25937  2sqmod  25940  chebbnd1lem2  25974  chebbnd1lem3  25975  rplogsumlem1  25988  rpvmasumlem  25991  dchrvmasumlem1  25999  dchrvmasum2lem  26000  dchrvmasumlema  26004  dchrisum0flblem2  26013  dchrisum0fno1  26015  dchrisum0re  26017  logdivsum  26037  pntrsumbnd2  26071  pntpbnd1a  26089  pntpbnd1  26090  pntibndlem2  26095  pntlemr  26106  pntlemj  26107  pntlemf  26109  pnt2  26117  padicabv  26134  ostth2lem2  26138  f1otrg  26585  brbtwn2  26619  colinearalglem2  26621  axcgrtr  26629  axcgrid  26630  axsegconlem7  26637  axsegcon  26641  ax5seglem3  26645  ax5seglem6  26648  ax5seg  26652  axpaschlem  26654  axlowdimlem17  26672  axcontlem2  26679  axcontlem4  26681  axcontlem7  26684  axcontlem8  26685  ecgrtg  26697  usgredg2v  26937  vtxdgoddnumeven  27263  2trlond  27646  eupthp1  27923  nmobndi  28480  ubthlem2  28576  ubthlem3  28577  minvecolem2  28580  shuni  29005  pjhthlem1  29096  chscllem2  29343  pjcompi  29377  mayete3i  29433  unoplin  29625  hmoplin  29647  nmophmi  29736  mdslmd4i  30038  isoun  30364  xrge0addcld  30413  xrofsup  30419  eliccelico  30427  elicoelioo  30428  difioo  30432  rexdiv  30530  xrge0addgt0  30606  omndadd2d  30637  omndadd2rd  30638  omndmul2  30641  cycpmcl  30686  cycpm2tr  30689  cyc3evpm  30720  cycpmconjslem2  30725  freshmansdream  30787  ofldchr  30815  qusker  30846  eqgvscpbl  30847  isprmidlc  30882  qsidomlem1  30883  lindsunlem  30920  finexttrb  30952  mdetpmtr2  30989  mdetpmtr12  30990  madjusmdetlem1  30992  madjusmdetlem4  30995  unitdivcld  31044  xrge0mulc1cn  31084  qqhnm  31131  esumcst  31222  esumfsup  31229  esumpmono  31238  esumcvg  31245  difelsiga  31292  sigapisys  31314  sigapildsys  31321  ldgenpisyslem1  31322  1stmbfm  31418  2ndmbfm  31419  dya2icoseg  31435  sibfinima  31497  probmeasb  31588  orvcgteel  31625  orvclteel  31630  ballotlemsima  31673  ballotlemfrceq  31686  sgnmul  31700  ccatmulgnn0dir  31712  fct2relem  31768  ftc2re  31769  chtvalz  31800  subfacp1lem2a  32325  subfaclim  32333  erdsze2lem2  32349  cvmliftlem2  32431  cvmliftlem10  32439  cvmliftlem13  32441  cvmliftiota  32446  cvmlift2lem9  32456  cvmlift2lem11  32458  cvmlift2lem12  32459  cvmliftphtlem  32462  cvmlift3lem6  32469  cvmlift3lem7  32470  cvmlift3lem9  32472  snmlff  32474  mrsubfval  32653  trpredelss  32969  trpredpo  32972  wzel  33009  wsuclem  33010  sltrec  33176  brsegle  33467  opnregcld  33576  fin2so  34761  poimirlem17  34791  poimirlem23  34797  opnmbllem0  34810  mblfinlem3  34813  mblfinlem4  34814  itg2addnclem  34825  itg2addnc  34828  itg2gt0cn  34829  ftc1cnnclem  34847  ftc1cnnc  34848  areacirclem5  34868  indexdom  34892  sstotbnd2  34935  isbnd3  34945  isbnd3b  34946  cntotbnd  34957  ismtyima  34964  heibor1lem  34970  heiborlem8  34979  rrncmslem  34993  reheibor  35000  lkrlsp  36120  lshpkrlem5  36132  ldualssvscl  36176  ldualssvsubcl  36177  llnmlplnN  36557  llncvrlpln  36576  pmapjat1  36871  pclfinN  36918  lautlt  37109  lauteq  37113  lautco  37115  ltrn11  37144  ltrnle  37147  ltrneq2  37166  cdlemednuN  37318  cdleme20k  37337  cdleme20l2  37339  cdleme20l  37340  cdleme20m  37341  cdleme21c  37345  cdleme22e  37362  cdleme22eALTN  37363  cdlemefrs32fva  37418  cdlemg4g  37634  cdlemg18b  37697  cdlemg18c  37698  cdlemj3  37841  dia2dimlem5  38086  dvhopN  38134  cdlemm10N  38136  dihjatcclem4  38439  dochexmidlem2  38479  lclkrlem2o  38539  lcfrlem5  38564  lcfrlem6  38565  lcdlssvscl  38624  mapdpglem6  38696  mapdpglem9  38698  mapdpglem12  38701  mapdpglem14  38703  mapdindp0  38737  hdmaprnlem7N  38873  hdmaprnlem8N  38874  hdmaprnlem3eN  38876  hgmapvvlem3  38943  mzpsubst  39225  eldioph2lem1  39237  eldioph2lem2  39238  eldioph2b  39240  diophin  39249  irrapxlem2  39300  irrapxlem4  39302  irrapxlem5  39303  pellexlem1  39306  pellexlem2  39307  pellexlem6  39311  elpell1qr2  39349  pell1qrgaplem  39350  pell1qrgap  39351  pellqrex  39356  pellfundex  39363  pellfund14  39375  rmspecsqrtnq  39383  rmxyadd  39398  congsub  39447  mzpcong  39449  congrep  39450  acongtr  39455  acongrep  39457  jm2.19lem1  39466  jm2.22  39472  jm2.23  39473  jm2.26lem3  39478  jm2.26  39479  jm2.27a  39482  fnwe2lem2  39531  aomclem6  39539  hbtlem2  39604  hbtlem4  39606  hbtlem5  39608  dgraa0p  39629  rngunsnply  39653  proot1hash  39680  itgpowd  39701  expgrowth  40547  fpmd  41418  abslt2sqd  41508  ioondisj2  41647  ioondisj1  41648  eliocre  41665  ioossioobi  41673  iooiinicc  41698  iooiinioc  41712  icossico2  41720  lptioo2  41792  limcresiooub  41803  limsupequzlem  41883  xlimmnfvlem2  41994  xlimpnfvlem2  41998  cncfuni  42049  cncfiooicclem1  42056  cxpcncf2  42063  dvcnre  42080  dvresntr  42082  dvmptresicc  42084  dvresioo  42086  dvbdfbdioolem1  42093  dvnmptdivc  42103  dvnxpaek  42107  itgsinexplem1  42119  itgcoscmulx  42134  itgiccshift  42145  itgperiod  42146  ovolsplit  42154  stoweidlem11  42177  stoweidlem26  42192  stoweidlem34  42200  stoweidlem36  42202  stoweidlem38  42204  stirlinglem5  42244  dirkercncflem2  42270  dirkercncflem4  42272  fourierdlem20  42293  fourierdlem58  42330  fourierdlem72  42344  fourierdlem73  42345  fourierdlem74  42346  fourierdlem75  42347  fourierdlem76  42348  fourierdlem79  42351  fourierdlem80  42352  fourierdlem87  42359  fourierdlem94  42366  fourierdlem103  42375  fourierdlem104  42376  fourierdlem107  42379  fourierdlem113  42385  sqwvfoura  42394  sqwvfourb  42395  fourierswlem  42396  fouriersw  42397  etransclem46  42446  etransclem47  42447  rrndistlt  42456  rrnprjdstle  42467  ioorrnopnxrlem  42472  sge0ssre  42560  sge0seq  42609  hsphoidmvle2  42748  hsphoidmvle  42749  hoidmv1lelem1  42754  hoidmv1lelem2  42755  hoidmv1lelem3  42756  hoidmvlelem1  42758  hoidifhspdmvle  42783  hoiqssbllem2  42786  ovolval5lem2  42816  iinhoiicc  42837  iunhoiioo  42839  vonioolem2  42844  vonicclem2  42847  issmflem  42885  iccpartdisj  43444  m1expevenALTV  43659  fpprel2  43753  tgoldbach  43829  strisomgrop  43852  nn0eo  44486  fdivpm  44501  refdivpm  44502  elbigolo1  44515  logbpw2m1  44525  fllog2  44526  dignn0flhalflem1  44573  dignn0flhalflem2  44574  itsclinecirc0in  44660  2itscplem2  44664  itscnhlinecirc02plem1  44667
  Copyright terms: Public domain W3C validator