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

Theorem syl22anc 1220
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 532 . 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 1217 1  |-  ( ph  ->  et )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
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 185  df-an 371
This theorem is referenced by:  fr2nr  4805  soltmin  5344  f1oprg  5788  fveqf1o  6108  weniso  6153  fr3nr  6500  smogt  6937  smorndom  6938  oacomf1o  7113  th3qlem1  7315  difsnen  7502  undom  7508  enfixsn  7529  domss2  7579  ssenen  7594  marypha1lem  7793  fisupcl  7827  ordtypelem3  7844  ordtypelem8  7849  oieu  7863  oismo  7864  wofib  7869  wemaplem2  7871  wemapso  7875  wemapso2OLD  7876  wemapso2lem  7877  unxpwdom2  7913  infdifsn  7972  oemapvali  8002  cantnflem1c  8005  cantnflem1d  8006  cantnflem1  8007  cantnf  8011  cantnfOLD  8033  cnfcom3  8047  cnfcom3OLD  8055  r1ordg  8095  dif1card  8287  infxpenlem  8290  dfac8clem  8312  infxp  8494  infmap2  8497  cflim2  8542  coftr  8552  fin2i2  8597  enfin2i  8600  fin23lem26  8604  fin23lem27  8607  fin23lem40  8630  isf32lem2  8633  isf32lem3  8634  isf32lem4  8635  isf32lem7  8638  isf32lem9  8640  fin1a2lem13  8691  fin12  8692  alephexp1  8853  gchdomtri  8906  fpwwe2lem12  8918  fpwwe2lem13  8919  gchpwdom  8947  gchhar  8956  adderpqlem  9233  mulerpqlem  9234  addassnq  9237  mulassnq  9238  distrnq  9240  mulidnq  9242  recmulnq  9243  ltexnq  9254  distrlem1pr  9304  distrlem4pr  9305  prlem936  9326  reclem3pr  9328  mulgt0d  9636  mul4d  9691  add4d  9703  add42d  9704  subcan  9774  addsub4d  9876  subadd4d  9877  sub4d  9878  2addsubd  9879  addsubeq4d  9880  muladdd  9912  mulsubd  9913  addgegt0d  10023  addge0d  10025  mulge0d  10026  le2addd  10067  le2subd  10068  ltleaddd  10069  leltaddd  10070  lt2subd  10072  divdivdiv  10142  divcan5  10143  divne0d  10233  recdivd  10234  recdiv2d  10235  divcan6d  10236  ddcand  10237  rec11d  10238  divmuldivd  10258  divmul13d  10259  divmul24d  10260  divadddivd  10261  divsubdivd  10262  divmuleqd  10263  divdivdivd  10264  subrecd  10272  mulge0b  10309  recreclt  10341  divgt0d  10378  mulgt1d  10379  lemulge11d  10380  lemulge12d  10381  ltmul12ad  10384  lemul12ad  10385  lemul12bd  10386  supmul1  10405  nndivtr  10473  qreccl  11083  ledivdivd  11162  lediv12ad  11192  lt2mul2divd  11195  xlt2add  11333  supxrun  11388  supxrre  11400  infmxrre  11408  iccss2  11476  iccssico2  11479  lincmb01cmp  11544  iccf1o  11545  fzrev2i  11637  modaddmodup  11878  modaddmodlo  11879  modsubdir  11883  fzennn  11906  sermono  11954  mulexpz  12020  expaddz  12024  ltexp2a  12031  leexp2a  12035  sqdiv  12047  expmulnbnd  12112  digit1  12114  expsubd  12135  lt2sqd  12158  le2sqd  12159  sq11d  12160  bcm1k  12207  bcp1n  12208  bcp1nk  12209  hashf1lem1  12325  cshw1  12573  2swrd2eqwrdeq  12670  absrele  12914  sqreulem  12964  sqrmuld  13028  sqrsq2d  13029  sqrled  13030  sqrltd  13031  sqr11d  13032  abs3lemd  13064  rlimuni  13145  climuni  13147  lo1resb  13159  o1resb  13161  2clim  13167  addcn2  13188  mulcn2  13190  o1of2  13207  o1rlimmul  13213  lo1add  13221  lo1mul  13222  isercolllem1  13259  caucvgrlem  13267  iseraltlem2  13277  iseraltlem3  13278  iseralt  13279  mptfzshft  13362  fsumrev  13363  fsum0diag2  13367  binomlem  13409  climcndslem1  13429  climcndslem2  13430  harmonic  13438  mertenslem1  13461  efcllem  13480  moddvds  13659  dvds1  13698  dvdsext  13701  oexpneg  13712  bitsinv1  13755  sadaddlem  13779  sadasslem  13783  sadeq  13785  mulgcd  13847  dvdssqlem  13860  rpmulgcd2  13908  isprm6  13912  isprm5  13915  crt  13970  eulerthlem2  13974  prmdiveq  13978  pythagtriplem11  14009  pythagtriplem13  14011  iserodd  14019  pcgcd1  14060  pcprmpw2  14065  pcaddlem  14067  fldivp1  14076  4sqlem12  14134  4sqlem14  14136  4sqlem15  14137  4sqlem16  14138  vdwapun  14152  mreexexlem4d  14703  acsfn1  14717  acsfn2  14719  sscpwex  14846  rescabs  14864  catciso  15093  yonedainv  15209  subm0  15602  pmtrff1o  16087  pmtrfcnv  16088  pmtrfb  16089  psgnunilem1  16117  odmodnn0  16163  odeq  16173  dfod2  16185  sylow1lem1  16217  lsmsubg  16273  lsmmod  16292  lsmdisj2  16299  ghmplusg  16448  odadd  16452  gexexlem  16454  lt6abl  16491  cyggex2  16493  dprdfinv  16630  dmdprdsplitlem  16655  dpjidcl  16678  ablfacrp  16688  ablfacrp2  16689  ablfac1c  16693  ablfac1eu  16695  lcomfsupOLD  17106  lcomfsupp  17107  lssvancl1  17148  lssvnegcl  17159  lspprvacl  17202  lspsneli  17204  lspsn  17205  lmhmplusg  17247  lmhmima  17250  lmhmpreima  17251  reslmhm  17255  lbsind2  17284  lsmcl  17286  lsmelval2  17288  lsppreli  17293  lspprabs  17298  pj1lmhm  17303  lssvs0or  17313  lspabs3  17324  lspfixed  17331  lspexch  17332  lsmcv  17344  lspsolv  17346  lidlmcl  17421  drngnidl  17433  2idlcpbl  17438  mplbas2  17674  mplbas2OLD  17675  evlslem3  17723  evlslem1  17724  coe1addfv  17841  evl1addd  17899  evl1subd  17900  evl1muld  17901  gzrngunit  18002  zringlpirlem3  18029  zlpirlem3  18034  prmirredlem  18041  prmirredlemOLD  18044  znf1o  18108  znunithash  18121  evpmodpmf1o  18150  frlmsubgval  18316  frlmvscaval  18318  frlmphllem  18329  frlmphl  18330  frlmssuvc1  18343  frlmssuvc1OLD  18345  frlmsslsp  18347  frlmsslspOLD  18348  frlmup1  18350  frlmup2  18351  lindfind2  18371  lindfrn  18374  f1lindf  18375  islindf4  18391  mamudi  18431  mamudir  18432  1marepvmarrepid  18512  mdetrlin  18539  smadiadetglem1  18608  smadiadetg  18610  cramerimplem1  18620  ntrin  18796  topssnei  18859  restbas  18893  restntr  18917  cnntri  19006  fiuncmp  19138  nllyrest  19221  nllyidm  19224  hausllycmp  19229  cldllycmp  19230  hauspwdom  19236  txcld  19307  txcn  19330  txlly  19340  txnlly  19341  txhaus  19351  txlm  19352  txkgen  19356  xkococnlem  19363  cnmpt2res  19381  xkoinjcn  19391  basqtop  19415  qtopeu  19420  qtophmeo  19521  trfbas2  19547  neifil  19584  hausflim  19685  alexsubALTlem2  19751  cnextfval  19765  cnextfvval  19768  cnextf  19769  clssubg  19810  utop2nei  19956  utop3cls  19957  utopreg  19958  psmetlecl  20022  xmetlecl  20052  prdsxmetlem  20074  bldisj  20104  imasf1obl  20194  prdsbl  20197  stdbdmet  20222  stdbdmopn  20224  met2ndci  20228  metcnp  20247  metusttoOLD  20263  metustto  20264  metustexhalfOLD  20269  metustexhalf  20270  cfilucfilOLD  20275  cfilucfil  20276  metucnOLD  20294  metucn  20295  lssnlm  20412  nmotri  20449  nmoid  20452  tgioo  20504  blcvx  20506  xrsmopn  20520  reperflem  20526  reconnlem2  20535  opnreen  20539  metdsge  20556  metdsre  20560  metdscnlem  20562  metnrmlem1a  20565  metnrmlem1  20566  metnrmlem3  20568  cncfmet  20615  cnmpt2pc  20631  icopnfcnv  20645  icopnfhmeo  20646  cnllycmp  20659  evth  20662  lebnumii  20669  nmoleub2lem3  20801  iscfil2  20908  cfil3i  20911  iscfil3  20915  cfilfcls  20916  iscau3  20920  iscmet3lem2  20934  caubl  20949  lmcau  20954  rrxcph  21027  minveclem2  21044  pjthlem1  21055  pjthlem2  21056  ivthicc  21073  ovollecl  21097  ovolunlem1a  21110  ovolunnul  21114  ovoliunlem1  21116  ismbl2  21141  nulmbl2  21150  unmbl  21151  volun  21158  voliunlem2  21164  ioombl1lem2  21172  uniioombllem2a  21194  uniioombllem3  21197  uniioombllem4  21198  dyaddisjlem  21207  dyadmaxlem  21209  opnmbllem  21213  volsup2  21217  volcn  21218  ismbfd  21250  mbfi1fseqlem1  21325  mbfi1fseqlem5  21329  itg2lecl  21348  itg2monolem2  21361  itg2gt0  21370  itgspliticc  21446  ellimc3  21486  limcres  21493  dvfval  21504  dvres3  21520  dvres3a  21521  dvnff  21529  dvnadd  21535  dvn2bss  21536  dvnres  21537  dvcmul  21550  dvcmulf  21551  dvmptres3  21562  dvmptres2  21568  dvmptntr  21577  dvexp3  21582  dvferm1lem  21588  dvlip  21597  dvlipcn  21598  dvlip2  21599  c1liplem1  21600  dvgt0lem1  21606  dvgt0lem2  21607  dvne0  21615  lhop1lem  21617  lhop2  21619  lhop  21620  dvcnvrelem1  21621  dvcnvrelem2  21622  dvcvx  21624  dvfsumle  21625  dvfsumabs  21627  dvfsumlem2  21631  ftc1lem6  21645  ftc1  21646  ftc2ditglem  21649  itgsubstlem  21652  tdeglem4  21661  mdegaddle  21677  mdegmullem  21681  ply1rem  21767  fta1glem2  21770  fta1blem  21772  ig1peu  21775  ig1pdvds  21780  dgrmulc  21870  dgrcolem1  21872  plydivlem4  21894  plydiveu  21896  fta1lem  21905  vieta1lem1  21908  vieta1lem2  21909  plyexmo  21911  taylfvallem1  21954  taylfval  21956  tayl0  21959  taylplem1  21960  taylply2  21965  taylply  21966  dvtaylp  21967  dvntaylp  21968  dvntaylp0  21969  taylthlem1  21970  taylthlem2  21971  ulmcaulem  21991  ulmcau  21992  ulmcn  21996  ulmdvlem1  21997  radcnvlem1  22010  radcnvle  22017  psercn  22023  pserdvlem2  22025  pserdv  22026  abelth  22038  cosordlem  22119  tanregt0  22127  dvlog2lem  22229  efopn  22235  logtayllem  22236  logccv  22240  cxplt3  22277  cxpmul2zd  22293  cxpltd  22296  cxpled  22297  cxplt3d  22309  cxple3d  22310  dvsqr  22314  cxpcn3  22318  cxpaddle  22322  cxpeq  22327  angcan  22330  angvald  22332  ang180lem2  22338  ang180  22342  isosctrlem3  22350  dquartlem1  22378  atantayl2  22465  leibpilem1  22467  leibpi  22469  log2tlbnd  22472  birthdaylem3  22479  xrlimcnp  22494  efrlim  22495  o1cxp  22500  jensenlem2  22513  jensen  22514  fsumharmonic  22537  wilthlem1  22538  basellem3  22552  basellem6  22555  basellem8  22557  ppisval  22573  chtwordi  22626  ppiwordi  22632  mumullem2  22650  dvdsmulf1o  22666  fsumvma  22684  fsumvma2  22685  chpchtsum  22690  chpub  22691  logfacubnd  22692  dchrmulcl  22720  dchrinv  22732  dchrptlem1  22735  dchrptlem2  22736  sumdchr2  22741  dchr2sum  22744  bposlem7  22761  lgslem1  22767  lgslem3  22769  lgsdirprm  22800  lgsqrlem2  22813  lgseisenlem1  22820  lgseisenlem2  22821  lgseisenlem4  22823  lgseisen  22824  lgsquadlem1  22825  lgsquad2lem1  22829  lgsquad3  22832  m1lgs  22833  2sqlem7  22841  chebbnd1lem2  22851  chebbnd1lem3  22852  rplogsumlem1  22865  rpvmasumlem  22868  dchrvmasumlem1  22876  dchrvmasum2lem  22877  dchrvmasumlema  22881  dchrisum0flblem2  22890  dchrisum0fno1  22892  dchrisum0re  22894  logdivsum  22914  pntrsumbnd2  22948  pntpbnd1a  22966  pntpbnd1  22967  pntibndlem2  22972  pntlemr  22983  pntlemj  22984  pntlemf  22986  pnt2  22994  padicabv  23011  ostth2lem2  23015  f1otrg  23268  brbtwn2  23302  colinearalglem2  23304  axcgrtr  23312  axcgrid  23313  axsegconlem7  23320  axsegcon  23324  ax5seglem3  23328  ax5seglem6  23331  ax5seg  23335  axpaschlem  23337  axlowdimlem17  23355  axcontlem2  23362  axcontlem4  23364  axcontlem7  23367  axcontlem8  23368  ecgrtg  23380  usgraidx2v  23462  iseupa  23737  eupap1  23748  eupath2lem3  23751  nmobndi  24326  ubthlem2  24423  ubthlem3  24424  minvecolem2  24427  shuni  24854  pjhthlem1  24945  chscllem2  25192  pjcompi  25226  mayete3i  25282  mayete3iOLD  25283  unoplin  25475  hmoplin  25497  nmophmi  25586  mdslmd4i  25888  preqsnd  26052  isoun  26147  xrofsup  26205  eliccelico  26211  elicoelioo  26212  difioo  26216  rexdiv  26245  xrge0addgt0  26298  omndadd2d  26315  omndadd2rd  26316  unitdivcld  26475  xrge0mulc1cn  26515  qqhnm  26563  esumcst  26658  esumfsup  26663  esumpmono  26672  esumcvg  26679  difelsiga  26720  1stmbfm  26818  2ndmbfm  26819  dya2icoseg  26835  sibfinima  26868  probmeasb  26956  orvcgteel  26993  orvclteel  26998  ballotlemsima  27041  ballotlemfrceq  27054  sgnmul  27068  ccatmulgnn0dir  27083  ofccat  27084  lgamucov  27167  lgamcvg2  27184  subfacp1lem2a  27211  subfaclim  27219  erdsze2lem2  27235  cvmliftlem2  27318  cvmliftlem10  27326  cvmliftlem13  27328  cvmliftiota  27333  cvmlift2lem9  27343  cvmlift2lem11  27345  cvmlift2lem12  27346  cvmliftphtlem  27349  cvmlift3lem6  27356  cvmlift3lem7  27357  cvmlift3lem9  27359  snmlff  27361  fprodser  27605  fprodshft  27630  fprodrev  27631  rprisefaccl  27669  trpredelss  27839  trpredpo  27842  wzel  27904  wsuclem  27905  nodenselem5  27969  nobndlem6  27981  brsegle  28282  fin2so  28563  opnmbllem0  28574  mblfinlem3  28577  mblfinlem4  28578  itg2addnclem  28590  itg2addnc  28593  itg2gt0cn  28594  ftc1cnnclem  28612  ftc1cnnc  28613  areacirclem5  28635  opnregcld  28672  indexdom  28775  sstotbnd2  28820  isbnd3  28830  isbnd3b  28831  cntotbnd  28842  ismtyima  28849  heibor1lem  28855  heiborlem8  28864  rrncmslem  28878  reheibor  28885  mzpsubst  29232  eldioph2lem1  29245  eldioph2lem2  29246  eldioph2b  29248  diophin  29258  irrapxlem2  29311  irrapxlem4  29313  irrapxlem5  29314  pellexlem1  29317  pellexlem2  29318  pellexlem6  29322  elpell1qr2  29360  pell1qrgaplem  29361  pell1qrgap  29362  pellqrex  29367  pellfundex  29374  pellfund14  29386  rmspecsqrnq  29394  rmxyadd  29409  expmordi  29435  rmxypos  29437  jm2.24  29453  congsub  29460  mzpcong  29462  congrep  29463  acongtr  29468  acongrep  29470  jm2.19lem1  29485  jm2.22  29491  jm2.23  29492  jm2.26lem3  29497  jm2.26  29498  jm2.27a  29501  fnwe2lem2  29551  aomclem6  29559  hbtlem2  29627  hbtlem4  29629  hbtlem5  29631  dgraa0p  29653  rngunsnply  29677  acsfn1p  29703  proot1hash  29715  itgpowd  29737  expgrowth  29756  itgsinexplem1  29941  stoweidlem11  29953  stoweidlem26  29968  stoweidlem34  29976  stoweidlem36  29978  stoweidlem38  29980  stirlinglem5  30020  numclwwlkovf2ex  30826  lply1binom  31008  mat2pmatscmxcl  31215  m2pmfzgsumcl  31231  m2cpminv  31234  pmatcollpw  31254  pmatcollpwfi  31255  pmatcollpw3fi1lem1  31258  cpmidpmatlem2  31342  cpmadugsumlemF  31347  chcoeffeqlem  31357  lkrlsp  33070  lshpkrlem5  33082  ldualssvscl  33126  ldualssvsubcl  33127  llnmlplnN  33506  llncvrlpln  33525  pmapjat1  33820  pclfinN  33867  lautlt  34058  lauteq  34062  lautco  34064  ltrn11  34093  ltrnle  34096  ltrneq2  34115  cdlemednuN  34267  cdleme20k  34286  cdleme20l2  34288  cdleme20l  34289  cdleme20m  34290  cdleme21c  34294  cdleme22e  34311  cdleme22eALTN  34312  cdlemefrs32fva  34367  cdlemg4g  34583  cdlemg18b  34646  cdlemg18c  34647  cdlemj3  34790  dia2dimlem5  35036  dvhopN  35084  cdlemm10N  35086  dihjatcclem4  35389  dochexmidlem2  35429  lclkrlem2o  35489  lcfrlem5  35514  lcfrlem6  35515  lcdlssvscl  35574  mapdpglem6  35646  mapdpglem9  35648  mapdpglem12  35651  mapdpglem14  35653  mapdindp0  35687  hdmaprnlem7N  35826  hdmaprnlem8N  35827  hdmaprnlem3eN  35829  hgmapvvlem3  35896
  Copyright terms: Public domain W3C validator