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

Theorem syl22anc 1183
Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
Hypotheses
Ref Expression
sylXanc.1  |-  ( ph  ->  ps )
sylXanc.2  |-  ( ph  ->  ch )
sylXanc.3  |-  ( ph  ->  th )
sylXanc.4  |-  ( ph  ->  ta )
syl22anc.5  |-  ( ( ( ps  /\  ch )  /\  ( th  /\  ta ) )  ->  et )
Assertion
Ref Expression
syl22anc  |-  ( ph  ->  et )

Proof of Theorem syl22anc
StepHypRef Expression
1 sylXanc.1 . . 3  |-  ( ph  ->  ps )
2 sylXanc.2 . . 3  |-  ( ph  ->  ch )
31, 2jca 518 . 2  |-  ( ph  ->  ( ps  /\  ch ) )
4 sylXanc.3 . 2  |-  ( ph  ->  th )
5 sylXanc.4 . 2  |-  ( ph  ->  ta )
6 syl22anc.5 . 2  |-  ( ( ( ps  /\  ch )  /\  ( th  /\  ta ) )  ->  et )
73, 4, 5, 6syl12anc 1180 1  |-  ( ph  ->  et )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  fr2nr  4371  fr3nr  4571  soltmin  5082  fveqf1o  5806  weniso  5852  smogt  6384  smorndom  6385  oacomf1o  6563  th3qlem1  6764  difsnen  6944  undom  6950  domss2  7020  ssenen  7035  marypha1lem  7186  fisupcl  7218  ordtypelem3  7235  ordtypelem8  7240  oieu  7254  oismo  7255  wofib  7260  wemaplem2  7262  wemapso  7266  wemapso2  7267  unxpwdom2  7302  infdifsn  7357  cantnf  7395  cnfcom3  7407  r1ordg  7450  dif1card  7638  infxpenlem  7641  dfac8clem  7659  infxp  7841  infmap2  7844  cflim2  7889  coftr  7899  fin2i2  7944  enfin2i  7947  fin23lem26  7951  fin23lem27  7954  fin23lem40  7977  isf32lem2  7980  isf32lem3  7981  isf32lem4  7982  isf32lem7  7985  isf32lem9  7987  fin1a2lem13  8038  fin12  8039  alephexp1  8201  gchdomtri  8251  fpwwe2lem12  8263  fpwwe2lem13  8264  gchhar  8293  gchpwdom  8296  adderpqlem  8578  mulerpqlem  8579  addassnq  8582  mulassnq  8583  distrnq  8585  mulidnq  8587  recmulnq  8588  ltexnq  8599  distrlem1pr  8649  distrlem4pr  8650  prlem936  8671  reclem3pr  8673  mulgt0d  8971  mul4d  9024  add4d  9035  add42d  9036  subcan  9102  addsub4d  9204  subadd4d  9205  sub4d  9206  2addsubd  9207  addsubeq4d  9208  muladdd  9237  mulsubd  9238  addgegt0d  9346  addge0d  9348  mulge0d  9349  le2addd  9390  le2subd  9391  ltleaddd  9392  leltaddd  9393  lt2subd  9395  divdivdiv  9461  divcan5  9462  divne0d  9552  recdivd  9553  recdiv2d  9554  divcan6d  9555  ddcand  9556  rec11d  9557  divmuldivd  9577  divmul13d  9578  divmul24d  9579  divadddivd  9580  divsubdivd  9581  divmuleqd  9582  divdivdivd  9583  subrecd  9591  recreclt  9655  divgt0d  9692  mulgt1d  9693  lemulge11d  9694  lemulge12d  9695  ltmul12ad  9698  lemul12ad  9699  lemul12bd  9700  supmul1  9719  nndivtr  9787  qreccl  10336  ledivdivd  10415  lediv12ad  10445  lt2mul2divd  10448  xlt2add  10580  supxrun  10634  supxrre  10646  infmxrre  10654  iccss2  10720  iccssico2  10723  lincmb01cmp  10777  iccf1o  10778  fzrev2i  10848  modsubdir  11008  fzennn  11030  sermono  11078  mulexpz  11142  expaddz  11146  ltexp2a  11153  leexp2a  11157  sqdiv  11169  expmulnbnd  11233  digit1  11235  expsubd  11256  lt2sqd  11279  le2sqd  11280  sq11d  11281  bcm1k  11327  bcp1n  11328  bcp1nk  11329  hashf1lem1  11393  absrele  11793  sqreulem  11843  sqrmuld  11907  sqrsq2d  11908  sqrled  11909  sqrltd  11910  sqr11d  11911  abs3lemd  11943  rlimuni  12024  climuni  12026  lo1resb  12038  o1resb  12040  2clim  12046  addcn2  12067  mulcn2  12069  o1of2  12086  o1rlimmul  12092  lo1add  12100  lo1mul  12101  isercolllem1  12138  caucvgrlem  12145  iseraltlem2  12155  iseraltlem3  12156  iseralt  12157  fsumrev  12241  fsumshft  12242  fsum0diag2  12245  binomlem  12287  climcndslem1  12308  climcndslem2  12309  harmonic  12317  mertenslem1  12340  efcllem  12359  moddvds  12538  dvds1  12577  dvdsext  12579  oexpneg  12590  bitsinv1  12633  sadaddlem  12657  sadasslem  12661  sadeq  12663  mulgcd  12725  dvdssqlem  12738  rpmulgcd2  12784  isprm6  12788  isprm5  12791  crt  12846  eulerthlem2  12850  prmdiveq  12854  pythagtriplem11  12878  pythagtriplem13  12880  iserodd  12888  pcgcd1  12929  pcprmpw2  12934  pcaddlem  12936  fldivp1  12945  4sqlem12  13003  4sqlem14  13005  4sqlem15  13006  4sqlem16  13007  vdwapun  13021  mreexexlem4d  13549  acsfn1  13563  acsfn2  13565  sscpwex  13692  rescabs  13710  catciso  13939  yonedainv  14055  p0le  14149  ple1  14150  subm0  14433  odmodnn0  14855  odeq  14865  dfod2  14877  sylow1lem1  14909  lsmsubg  14965  lsmmod  14984  lsmdisj2  14991  ghmplusg  15138  odadd  15142  gexexlem  15144  lt6abl  15181  cyggex2  15183  ablfacrp  15301  ablfacrp2  15302  ablfac1c  15306  ablfac1eu  15308  lssvancl1  15702  lssvnegcl  15713  lspprvacl  15756  lspsneli  15758  lspsn  15759  lmhmplusg  15801  lmhmima  15804  lmhmpreima  15805  reslmhm  15809  lbsind2  15834  lsmcl  15836  lsmelval2  15838  lsppreli  15843  lspprabs  15848  pj1lmhm  15853  lssvs0or  15863  lspabs3  15874  lspfixed  15881  lspexch  15882  lsmcv  15894  lspsolv  15896  lidlmcl  15969  drngnidl  15981  2idlcpbl  15986  mplbas2  16212  coe1addfv  16342  gzrngunit  16437  zlpirlem3  16443  prmirredlem  16446  znf1o  16505  znunithash  16518  ntrin  16798  topssnei  16861  restbas  16889  restntr  16912  cnntri  17000  fiuncmp  17131  nllyrest  17212  nllyidm  17215  hausllycmp  17220  cldllycmp  17221  hauspwdom  17227  txcld  17298  txcn  17320  txlly  17330  txnlly  17331  txhaus  17341  txlm  17342  txkgen  17346  xkococnlem  17353  cnmpt2res  17371  xkoinjcn  17381  basqtop  17402  qtopeu  17407  qtophmeo  17508  trfbas2  17538  neifil  17575  hausflim  17676  alexsubALTlem2  17742  clssubg  17791  xmetlecl  17911  prdsxmetlem  17932  bldisj  17955  imasf1obl  18034  prdsbl  18037  stdbdmet  18062  stdbdmopn  18064  met2ndci  18068  metcnp  18087  lssnlm  18211  nmotri  18248  nmoid  18251  tgioo  18302  blcvx  18304  xrsmopn  18318  reperflem  18323  reconnlem2  18332  opnreen  18336  metdsge  18353  metdsre  18357  metdscnlem  18359  metnrmlem1a  18362  metnrmlem1  18363  metnrmlem3  18365  cncfmet  18412  cnmpt2pc  18426  icopnfcnv  18440  icopnfhmeo  18441  cnllycmp  18454  evth  18457  lebnumii  18464  nmoleub2lem3  18596  iscfil2  18692  cfil3i  18695  iscfil3  18699  cfilfcls  18700  iscau3  18704  iscmet3lem2  18718  caubl  18733  lmcau  18738  minveclem2  18790  pjthlem1  18801  pjthlem2  18802  ivthicc  18818  ovollecl  18842  ovolunlem1a  18855  ovolunnul  18859  ovoliunlem1  18861  ismbl2  18886  nulmbl2  18894  unmbl  18895  volun  18902  voliunlem2  18908  ioombl1lem2  18916  uniioombllem2a  18937  uniioombllem3  18940  uniioombllem4  18941  dyaddisjlem  18950  dyadmaxlem  18952  opnmbllem  18956  volsup2  18960  volcn  18961  ismbfd  18995  mbfi1fseqlem1  19070  mbfi1fseqlem5  19074  itg2lecl  19093  itg2monolem2  19106  itg2gt0  19115  itgspliticc  19191  ellimc3  19229  limcres  19236  dvfval  19247  dvres3  19263  dvres3a  19264  dvnff  19272  dvnadd  19278  dvn2bss  19279  dvnres  19280  dvcmul  19293  dvcmulf  19294  dvmptres3  19305  dvmptres2  19311  dvmptntr  19320  dvexp3  19325  dvferm1lem  19331  dvlip  19340  dvlipcn  19341  dvlip2  19342  c1liplem1  19343  dvgt0lem1  19349  dvgt0lem2  19350  dvne0  19358  lhop1lem  19360  lhop2  19362  lhop  19363  dvcnvrelem1  19364  dvcnvrelem2  19365  dvcvx  19367  dvfsumle  19368  dvfsumabs  19370  dvfsumlem2  19374  ftc1lem6  19388  ftc1  19389  ftc2ditglem  19392  itgsubstlem  19395  evlslem3  19398  evlslem1  19399  evl1addd  19417  evl1subd  19418  evl1muld  19419  mdegaddle  19460  mdegmullem  19464  ply1rem  19549  fta1glem2  19552  fta1blem  19554  ig1peu  19557  ig1pdvds  19562  dgrmulc  19652  dgrcolem1  19654  plydivlem4  19676  plydiveu  19678  fta1lem  19687  vieta1lem1  19690  vieta1lem2  19691  plyexmo  19693  taylfvallem1  19736  taylfval  19738  tayl0  19741  taylplem1  19742  taylply2  19747  taylply  19748  dvtaylp  19749  dvntaylp  19750  dvntaylp0  19751  taylthlem1  19752  taylthlem2  19753  ulmcaulem  19771  ulmcau  19772  ulmcn  19776  ulmdvlem1  19777  radcnvlem1  19789  radcnvle  19796  psercn  19802  pserdvlem2  19804  pserdv  19805  abelth  19817  cosordlem  19893  tanregt0  19901  dvlog2lem  19999  efopn  20005  logtayllem  20006  logccv  20010  cxplt3  20047  cxpmul2zd  20063  cxpltd  20066  cxpled  20067  cxplt3d  20079  cxple3d  20080  dvsqr  20084  cxpcn3  20088  cxpaddle  20092  cxpeq  20097  angcan  20100  angvald  20102  ang180lem2  20108  ang180lem4  20110  ang180  20112  lawcos  20114  isosctrlem3  20120  dquartlem1  20147  atantayl2  20234  leibpilem1  20236  leibpi  20238  log2tlbnd  20241  birthdaylem3  20248  xrlimcnp  20263  efrlim  20264  o1cxp  20269  jensenlem2  20282  jensen  20283  fsumharmonic  20305  wilthlem1  20306  basellem3  20320  basellem6  20323  basellem8  20325  ppisval  20341  chtwordi  20394  ppiwordi  20400  mumullem2  20418  dvdsmulf1o  20434  fsumvma  20452  fsumvma2  20453  chpchtsum  20458  chpub  20459  logfacubnd  20460  dchrmulcl  20488  dchrinv  20500  dchrptlem1  20503  dchrptlem2  20504  sumdchr2  20509  dchr2sum  20512  bposlem7  20529  lgslem1  20535  lgslem3  20537  lgsdirprm  20568  lgsqrlem2  20581  lgseisenlem1  20588  lgseisenlem2  20589  lgseisenlem4  20591  lgseisen  20592  lgsquadlem1  20593  lgsquad2lem1  20597  lgsquad3  20600  m1lgs  20601  2sqlem7  20609  chebbnd1lem2  20619  chebbnd1lem3  20620  rplogsumlem1  20633  rpvmasumlem  20636  dchrvmasumlem1  20644  dchrvmasum2lem  20645  dchrvmasumlema  20649  dchrisum0flblem2  20658  dchrisum0fno1  20660  dchrisum0re  20662  logdivsum  20682  pntrsumbnd2  20716  pntpbnd1a  20734  pntpbnd1  20735  pntibndlem2  20740  pntlemr  20751  pntlemj  20752  pntlemf  20754  pnt2  20762  padicabv  20779  ostth2lem2  20783  nmobndi  21353  ubthlem2  21450  ubthlem3  21451  minvecolem2  21454  shuni  21879  pjhthlem1  21970  chscllem2  22217  pjcompi  22251  mayete3i  22307  mayete3iOLD  22308  unoplin  22500  hmoplin  22522  nmophmi  22611  mdslmd4i  22913  ballotlemsima  23074  ballotlemfrceq  23087  rexdiv  23109  preqsnd  23194  isoun  23242  xrofsup  23255  eliccelico  23270  elicoelioo  23271  difioo  23275  unitdivcld  23285  xrge0mulc1cn  23323  xrge0addgt0  23331  esumcst  23436  esumpcvgval  23446  esumpmono  23447  esumcvg  23454  difelsiga  23494  dya2iocseg  23579  probmeasb  23633  orvcgteel  23668  orvclteel  23673  subfacp1lem2a  23711  subfaclim  23719  erdsze2lem2  23735  cvmliftlem2  23817  cvmliftlem10  23825  cvmliftlem13  23827  cvmliftiota  23832  cvmlift2lem9  23842  cvmlift2lem11  23844  cvmlift2lem12  23845  cvmliftphtlem  23848  cvmlift3lem6  23855  cvmlift3lem7  23856  cvmlift3lem9  23858  iseupa  23881  eupap1  23900  eupath2lem3  23903  snmlff  23912  mulge0b  24086  trpredelss  24235  trpredpo  24238  nodenselem5  24339  nobndlem6  24351  brbtwn2  24533  colinearalglem2  24535  axcgrtr  24543  axcgrid  24544  axsegconlem7  24551  axsegcon  24555  ax5seglem3  24559  ax5seglem6  24562  ax5seg  24566  axpaschlem  24568  axlowdimlem17  24586  axcontlem2  24593  axcontlem4  24595  axcontlem7  24598  axcontlem8  24599  brsegle  24731  bpoly3  24793  areacirclem6  24930  infxpg  25095  curgrpact  25372  limptlimpr2lem1  25574  limptlimpr2lem2  25575  cntrset  25602  opnregcld  26248  indexdom  26413  sstotbnd2  26498  isbnd3  26508  isbnd3b  26509  cntotbnd  26520  ismtyima  26527  heibor1lem  26533  heiborlem8  26542  rrncmslem  26556  reheibor  26563  lcomfsup  26768  mzpsubst  26826  eldioph2lem1  26839  eldioph2lem2  26840  eldioph2b  26842  diophin  26852  irrapxlem2  26908  irrapxlem4  26910  irrapxlem5  26911  pellexlem1  26914  pellexlem2  26915  pellexlem6  26919  elpell1qr2  26957  pell1qrgaplem  26958  pell1qrgap  26959  pellqrex  26964  pellfundex  26971  pellfund14  26983  rmspecsqrnq  26991  rmxyadd  27006  expmordi  27032  rmxypos  27034  jm2.24  27050  congsub  27057  mzpcong  27059  congrep  27060  acongtr  27065  acongrep  27067  jm2.19lem1  27082  jm2.22  27088  jm2.23  27089  jm2.26lem3  27094  jm2.26  27095  jm2.27a  27098  fnwe2lem2  27148  aomclem6  27156  frlmvscaval  27231  frlmssuvc1  27246  frlmsslsp  27248  frlmup1  27250  frlmup2  27251  enfixsn  27257  lindfind2  27288  lindfrn  27291  f1lindf  27292  islindf4  27308  hbtlem2  27328  hbtlem4  27330  hbtlem5  27332  dgraa0p  27354  rngunsnply  27378  pmtrff1o  27404  pmtrfcnv  27405  pmtrfb  27406  psgnunilem1  27416  mamudi  27461  mamudir  27462  acsfn1p  27507  proot1hash  27519  expgrowth  27552  f1oprg  28075  lkrlsp  29292  lshpkrlem5  29304  ldualssvscl  29348  ldualssvsubcl  29349  llnmlplnN  29728  llncvrlpln  29747  pmapjat1  30042  pclfinN  30089  lautlt  30280  lauteq  30284  lautco  30286  ltrn11  30315  ltrnle  30318  ltrneq2  30337  cdlemednuN  30489  cdleme20k  30508  cdleme20l2  30510  cdleme20l  30511  cdleme20m  30512  cdleme21c  30516  cdleme22e  30533  cdleme22eALTN  30534  cdlemefrs32fva  30589  cdlemg4g  30805  cdlemg18b  30868  cdlemg18c  30869  cdlemj3  31012  dia2dimlem5  31258  dvhopN  31306  cdlemm10N  31308  dihjatcclem4  31611  dochexmidlem2  31651  lclkrlem2o  31711  lcfrlem5  31736  lcfrlem6  31737  lcdlssvscl  31796  mapdpglem6  31868  mapdpglem9  31870  mapdpglem12  31873  mapdpglem14  31875  mapdindp0  31909  hdmaprnlem7N  32048  hdmaprnlem8N  32049  hdmaprnlem3eN  32051  hgmapvvlem3  32118
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator