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

Theorem syl12anc 1224
Description: Syllogism combined with contraction. (Contributed by Jeff Hankins, 1-Aug-2009.)
Hypotheses
Ref Expression
sylXanc.1  |-  ( ph  ->  ps )
sylXanc.2  |-  ( ph  ->  ch )
sylXanc.3  |-  ( ph  ->  th )
syl12anc.4  |-  ( ( ps  /\  ( ch 
/\  th ) )  ->  ta )
Assertion
Ref Expression
syl12anc  |-  ( ph  ->  ta )

Proof of Theorem syl12anc
StepHypRef Expression
1 sylXanc.1 . . 3  |-  ( ph  ->  ps )
2 sylXanc.2 . . 3  |-  ( ph  ->  ch )
3 sylXanc.3 . . 3  |-  ( ph  ->  th )
41, 2, 3jca32 533 . 2  |-  ( ph  ->  ( ps  /\  ( ch  /\  th ) ) )
5 syl12anc.4 . 2  |-  ( ( ps  /\  ( ch 
/\  th ) )  ->  ta )
64, 5syl 16 1  |-  ( ph  ->  ta )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367
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 369
This theorem is referenced by:  syl22anc  1227  raaan  3853  raaanv  3854  soltmin  5316  xpdifid  5345  f1dom3fv3dif  6076  cocan1  6095  fliftfun  6111  soisores  6124  soisoi  6125  isopolem  6142  f1oiso2  6149  weniso  6151  caovcld  6367  caovcomd  6370  onminex  6541  tfrlem12  6976  omeulem1  7149  oaabs2  7212  omabs  7214  erov  7326  findcard2d  7677  frfi  7680  finsschain  7742  suplub2  7835  supmaxOLD  7840  supgtoreq  7843  supisolem  7846  ordiso2  7855  ordtypelem7  7864  wemaplem2  7887  wemapsolem  7890  cantnflt  8004  cantnfp1lem3  8012  cantnflem1b  8018  cantnflem1  8021  cantnfltOLD  8034  cantnfp1lem3OLD  8038  cantnflem1bOLD  8041  cantnflem1OLD  8044  wemapwe  8052  wemapweOLD  8053  cnfcomlem  8056  cnfcom  8057  cnfcom3lem  8060  cnfcomlemOLD  8064  cnfcomOLD  8065  cnfcom3lemOLD  8068  infxpenlem  8304  fseqenlem1  8318  dfac12lem2  8437  infpssrlem4  8599  enfin2i  8614  isf34lem7  8672  isf34lem6  8673  fin1a2lem7  8699  fin1a2lem10  8702  fin1a2lem11  8703  fin1a2lem13  8705  ttukeylem6  8807  ttukeylem7  8808  iundom2g  8828  fpwwe2lem6  8924  fpwwe2lem7  8925  fpwwe2lem9  8927  fpwwe2lem12  8930  fpwwe2  8932  canthnumlem  8937  canthwelem  8939  canthp1lem2  8942  pwfseqlem4  8951  inar1  9064  intgru  9103  distrlem4pr  9315  conjmul  10178  lediv12a  10354  recp1lt1  10359  cju  10448  gtndiv  10857  zsupss  11090  uzsupss  11093  icc0  11498  iccssioo2  11518  fzrev3  11667  elfz1b  11670  ico01fl0  11853  fldiv  11887  modabs  11930  modltm1p1mod  11942  modifeq2int  11952  seqcaopr  12047  seqf1olem1  12049  seqof2  12068  crreczi  12193  seqcoll  12416  seqcoll2  12417  hashtpg  12427  swrdccat3b  12632  sqrlem2  13079  resqrex  13086  abs1m  13170  isercoll  13492  zsum  13542  fsum2dlem  13587  fsumcom2  13591  fprod2dlem  13786  fprodcom2  13790  efsub  13837  bitsinv2  14095  sqgcd  14198  qredeu  14250  pcpremul  14369  pceulem  14371  pczpre  14373  pcdiv  14378  pcqmul  14379  pcqdiv  14383  pcexp  14385  pcdvdsb  14394  pcneg  14399  pcdvdstr  14401  pcgcd1  14402  pc2dvds  14404  pcz  14406  pcaddlem  14409  pcadd  14410  qexpz  14422  expnprm  14423  infpnlem2  14431  ramub2  14534  ramub1lem1  14546  f1ocpbllem  14931  f1ovscpbl  14933  mreexexlem3d  15053  mreexexlem4d  15054  fthi  15324  ipodrsima  15912  mndpropd  16063  grpsubpropd2  16258  ghmf1  16412  symgfvne  16530  f1omvdmvd  16585  f1otrspeq  16589  pmtrdifwrdel  16627  pmtrdifwrdel2  16628  psgnunilem2  16637  psgnunilem3  16638  psgnvalii  16651  odf1  16701  lsmpropd  16812  gsummptshft  17072  dprdf1o  17192  pgpfac1lem3  17241  pgpfac1lem5  17243  pgpfaclem1  17245  ablfaclem2  17250  srgbinomlem3  17306  ringpropd  17343  f1rhm0to0  17502  lmodprop2d  17685  lsspropd  17776  lmhmpropd  17832  lbspropd  17858  lbsextlem3  17919  lidlsubclOLD  17977  assapropd  18089  psrass1  18173  psrass23l  18176  psrass23  18178  mplsubrg  18215  mplmon  18238  mplmonmul  18239  mplcoe1  18240  mplbas2  18247  mplind  18280  evlslem2  18293  mpfind  18318  gsumply1subr  18388  psrplusgpropd  18390  ply1scln0  18445  ply1coeOLD  18451  iporthcom  18761  obslbs  18852  scmataddcl  19103  scmatsubcl  19104  scmatmulcl  19105  smatvscl  19111  scmatrhmcl  19115  mat1scmat  19126  smadiadetglem2  19259  cramerimplem2  19271  cramerimplem3  19272  cramerimp  19273  1pmatscmul  19288  mat2pmatf1  19315  pm2mp  19411  chmatcl  19414  chmatval  19415  chmaidscmat  19434  chfacfisf  19440  cayhamlem1  19452  cpmidgsumm2pm  19455  cpmidpmat  19459  cpmadugsumfi  19463  cpmadumatpoly  19469  cayhamlem3  19473  pptbas  19594  elcls  19660  neiint  19691  neiptopnei  19719  restbas  19745  neitr  19767  iscnp4  19850  cnconst2  19870  cnpdis  19880  cnt0  19933  cnhaus  19941  cmpcovf  19977  hauscmplem  19992  concompid  20017  2ndci  20034  2ndc1stc  20037  1stcrest  20039  2ndcctbss  20041  2ndcomap  20044  2ndcsep  20045  dis2ndc  20046  restlly  20069  islly2  20070  lly1stc  20082  dislly  20083  finlocfin  20106  dissnlocfin  20115  locfindis  20116  llycmpkgen2  20136  ptbasfi  20167  neitx  20193  ptpjopn  20198  ptcnplem  20207  upxp  20209  txlly  20222  txtube  20226  tx1stc  20236  txkgen  20238  xkococnlem  20245  kqreglem1  20327  kqreglem2  20328  kqnrmlem1  20329  kqnrmlem2  20330  hmeoimaf1o  20356  reghmph  20379  nrmhmph  20380  ordthmeolem  20387  trfil2  20473  fmfnfm  20544  hauspwpwf1  20573  fclsfnflim  20613  cnextf  20651  cnextcn  20652  tmdgsum2  20680  symgtgp  20685  subgntr  20690  opnsubg  20691  ghmcnp  20698  qustgpopn  20703  tsmsf1o  20732  tsmsxplem1  20740  tsmsxplem2  20741  tsmsxp  20742  ustexsym  20803  restutop  20825  imasdsf1olem  20961  blssexps  21014  blssex  21015  ssblex  21016  imasf1oxms  21077  blcld  21093  stdbdmopn  21106  met1stc  21109  met2ndci  21110  prdsxmslem2  21117  metcnp3  21128  cfilucfilOLD  21157  cfilucfil  21158  ngptgp  21235  tgioo  21386  tgqioo  21390  zdis  21406  iccpnfhmeo  21530  xrhmeo  21531  cnheibor  21540  elpi1i  21631  cmetcuspOLD  21878  cmetcusp  21879  pjthlem2  21938  ivthlem2  21949  ovolicc1  22012  ovolicc2lem3  22015  ovolicc2lem4  22016  volsup  22051  volivth  22101  vitalilem3  22104  mbflimsup  22158  mbfi1fseqlem1  22207  mbfi1fseqlem3  22209  mbfi1fseqlem5  22211  limcnlp  22367  limcflf  22370  limciun  22383  dvmptfsum  22461  dvcnvlem  22462  dvcvx  22506  facth1  22650  elply2  22678  plypf1  22694  coeeq  22709  aaliou3lem8  22826  ulm2  22865  mtestbdd  22885  reeff1o  22927  dcubic2  23291  quart  23308  xrlimcnp  23415  amgm  23437  harmonicbnd4  23457  perfect  23623  dchrptlem1  23656  bposlem2  23677  lgsfcl2  23694  lgsdir  23722  lgsdi  23724  lgsne0  23725  dchrvmasumlem2  23800  chpdifbndlem2  23856  pntpbnd1  23888  pntpbnd2  23889  padicabv  23932  tgcgrxfr  24029  idmot  24044  legid  24094  btwnleg  24095  leg0  24099  tghilberti1  24137  mirreu3  24155  colperpex  24227  lnopp2hpgb  24252  axcgrrflx  24338  axsegconlem1  24341  axcontlem2  24389  axcontlem12  24399  eengtrkg  24409  nbgraf1olem5  24566  wwlknredwwlkn  24847  clwwlkel  24914  clwlkfclwwlk  24965  2spotiundisj  25183  numclwwlkovf2ex  25207  frgraogt3nreg  25241  subgoid  25426  subgoinv  25427  ghgrpOLD  25487  nvpi  25686  nmlno0lem  25825  fh1  26653  fh2  26654  eigposi  26871  nmlnop0iALT  27030  nmopun  27049  branmfn  27140  opsqrlem1  27175  opsqrlem6  27180  mdslmd1lem1  27360  csmdsymi  27369  atom1d  27388  chirredlem2  27426  cdj1i  27468  cdj3i  27476  fcnvgreu  27660  xrofsup  27735  2sqmod  27789  archirngz  27886  archiabllem2a  27891  gsummpt2d  27925  orngsqr  27948  ornglmullt  27951  orngrmullt  27952  metideq  28026  metider  28027  pstmfval  28029  lmxrge0  28088  qqhval2  28116  qqhf  28120  qqhghm  28122  qqhrhm  28123  esumpcvgval  28226  esum2dlem  28240  esum2d  28241  sigainb  28285  insiga  28286  ddemeas  28364  imambfm  28389  dya2icoseg  28404  dya2iocnrect  28408  eulerpartlemgvv  28498  probun  28541  ballotlemfc0  28614  ballotlemfcc  28615  sgnmul  28664  signstfvneq0  28712  erdszelem8  28831  erdszelem9  28832  erdsze2lem2  28837  cnpcon  28864  txpcon  28866  ptpcon  28867  indispcon  28868  conpcon  28869  cvxpcon  28876  cnllyscon  28879  cvmcov2  28909  cvmopnlem  28912  cvmliftmolem1  28915  cvmliftlem14  28931  cvmliftlem15  28932  cvmlift2lem13  28949  cvmlift3lem2  28954  cvmlift3lem9  28961  poseq  29498  sltres  29589  nodense  29614  nocvxmin  29616  nobndup  29625  nobnddown  29626  seglerflx  29915  seglemin  29916  btwnsegle  29920  hilbert1.1  29957  wl-2sb6d  30173  tan2h  30212  heicant  30214  mblfinlem2  30217  itg2addnc  30235  ftc2nc  30265  dvasin  30269  neibastop2lem  30344  sdclem1  30402  fdc  30404  istotbnd3  30433  sstotbnd  30437  prdstotbnd  30456  prdsbnd2  30457  cntotbnd  30458  rngoisocnv  30550  mzpcompact2lem  30849  diophrw  30857  rexrabdioph  30893  eldioph4b  30910  pellexlem5  30934  pellfund14  30999  acongtr  31081  fnwe2lem3  31164  gicabl  31215  hbtlem2  31241  hbtlem4  31243  hbtlem5  31245  dgraalem  31262  aaitgo  31279  ioounsn  31345  isprm7  31360  islptre  31791  limclner  31823  icccncfext  31856  stoweidlem1  31949  stoweidlem14  31962  stoweidlem24  31972  stoweidlem46  31994  stoweidlem57  32005  dirkercncflem2  32052  fourierdlem20  32075  fourierdlem41  32096  fourierdlem46  32101  fourierdlem48  32103  fourierdlem50  32105  fourierdlem62  32117  fourierdlem63  32118  fourierdlem64  32119  fourierdlem65  32120  fourierdlem76  32131  fourierdlem79  32134  fourierdlem103  32158  fourierdlem104  32159  etransclem47  32230  raaan2  32346  perfectALTV  32545  mgmpropd  32781  lidlmmgm  32931  gsumlsscl  33176  lincsumcl  33232  lincscmcl  33233  isldepslvec2  33286  m1modmmod  33334  elbigo2  33373  relogbdivb  33383  blennnt2  33410  dignn0ldlem  33423  bj-finsumval0  35010  lsmsat  35146  islfld  35200  ps-2  35615  lplnexllnN  35701  4atlem9  35740  4atlem10a  35741  lnatexN  35916  2lnat  35921  pmapjat1  35990  lhpj1  36159  lhpm0atN  36166  4atexlemex2  36208  4atex  36213  4atex2-0aOLDN  36215  4atex2-0cOLDN  36217  lautcnvle  36226  lautj  36230  lautm  36231  idltrn  36287  cdleme01N  36359  cdleme0ex1N  36361  cdleme5  36378  cdleme9  36391  cdleme11c  36399  cdleme11g  36403  cdlemefrs29bpre0  36535  cdlemefrs29cpre1  36537  cdlemefrs32fva1  36540  cdleme32fva  36576  cdleme32fva1  36577  cdleme32fvaw  36578  cdleme32d  36583  cdleme32f  36585  cdleme35fnpq  36588  cdleme48d  36674  cdleme48gfv  36676  cdleme50ltrn  36696  trlord  36708  cdlemg4b1  36748  cdlemg4b2  36749  cdlemg13a  36790  cdlemg17a  36800  cdlemg17f  36805  erng1lem  37126  erngdvlem3  37129  erngdvlem4  37130  erng1r  37134  erngdvlem3-rN  37137  erngdvlem4-rN  37138  dva0g  37167  dialss  37186  dia0  37192  dia1N  37193  diaglbN  37195  diameetN  37196  diainN  37197  diaintclN  37198  dia1dim  37201  dia2dimlem5  37208  dia2dimlem7  37210  dia2dimlem9  37212  dia2dimlem10  37213  dia2dimlem12  37215  dia2dimlem13  37216  dvhopvadd  37233  dvhvaddass  37237  dvhopvsca  37242  tendolinv  37245  tendorinv  37246  dvhlveclem  37248  dvh0g  37251  dvheveccl  37252  dvhopN  37256  docaclN  37264  diaocN  37265  djajN  37277  dib0  37304  dib1dim  37305  dibglbN  37306  dibintclN  37307  dib1dim2  37308  diblss  37310  diblsmopel  37311  dicvaddcl  37330  dicvscacl  37331  diclspsn  37334  cdlemn4a  37339  cdlemn11c  37349  dihjustlem  37356  dihord1  37358  dihord2a  37359  dihord2b  37360  dihord2cN  37361  dihord11b  37362  dihord11c  37364  dihord2pre  37365  dihlsscpre  37374  dih1dimb  37380  dib2dim  37383  dih2dimb  37384  dih2dimbALTN  37385  dihvalcq2  37387  dihopelvalcpre  37388  dihord6apre  37396  dihord5b  37399  dihord5apre  37402  dih0  37420  dihmeetlem1N  37430  dihglblem5apreN  37431  dihglblem3N  37435  dihmeetlem2N  37439  dihglbcpreN  37440  dihmeetlem4preN  37446  dih1dimatlem0  37468  dih1dimatlem  37469  dihatlat  37474  dihatexv  37478  dihglb2  37482  dihmeet  37483  dihintcl  37484  dihmeet2  37486  doch2val2  37504  dochocss  37506  dihoml4c  37516  dochdmj1  37530  djhlj  37541  djhljjN  37542  djhjlj  37543  dihsumssj  37548  djhexmid  37551  djhlsmcl  37554  djhcvat42  37555  dihjatcclem4  37561  dihjat1lem  37568  dihsmsprn  37570  dihjat3  37572  dvh3dim2  37588  dvh3dim3N  37589  dochkr1OLDN  37619  lclkrlem2c  37649  lclkrlem2d  37650  mapdpglem23  37834  hdmap11lem2  37985
  Copyright terms: Public domain W3C validator