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

Theorem syl112anc 1231
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 )
syl112anc.5  |-  ( ( ps  /\  ch  /\  ( th  /\  ta )
)  ->  et )
Assertion
Ref Expression
syl112anc  |-  ( ph  ->  et )

Proof of Theorem syl112anc
StepHypRef Expression
1 sylXanc.1 . 2  |-  ( ph  ->  ps )
2 sylXanc.2 . 2  |-  ( ph  ->  ch )
3 sylXanc.3 . . 3  |-  ( ph  ->  th )
4 sylXanc.4 . . 3  |-  ( ph  ->  ta )
53, 4jca 532 . 2  |-  ( ph  ->  ( th  /\  ta ) )
6 syl112anc.5 . 2  |-  ( ( ps  /\  ch  /\  ( th  /\  ta )
)  ->  et )
71, 2, 5, 6syl3anc 1227 1  |-  ( ph  ->  et )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 972
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  df-3an 974
This theorem is referenced by:  rmob2  3415  fveqf1o  6186  enfixsn  7624  gruina  9194  grur1  9196  enqeq  9310  recrec  10242  rec11r  10244  divdivdiv  10246  dmdcan  10255  ddcan  10259  rereccl  10263  div2neg  10268  divmuld  10343  divmul2d  10354  divmul3d  10355  divassd  10356  div12d  10357  div23d  10358  divdird  10359  divsubdird  10360  div11d  10361  ltmul12a  10399  ltdiv1  10407  ltrec  10427  lt2msq1  10429  lediv2  10436  supmul1  10509  qbtwnre  11402  xlemul1a  11484  xlemul1  11486  xadd4d  11499  quoremz  11956  quoremnn0ALT  11958  expgt1  12178  nnlesq  12245  expnbnd  12269  expmulnbnd  12272  discr1  12276  facubnd  12352  hashf1lem1  12478  2swrdeqwrdeq  12652  sqrlem6  13055  mulcn2  13392  climcnds  13637  geomulcvg  13659  cvgrat  13666  eftlub  13716  eflegeo  13728  tanhlt1  13767  sin01bnd  13792  cos01bnd  13793  eirrlem  13809  bitsmod  13958  mulgcd  14056  prmind2  14100  mulgcddvds  14117  qnumgt0  14155  iserodd  14231  pcpremul  14239  fldivp1  14288  pcfaclem  14289  qexpz  14292  prmpwdvds  14294  pockthg  14296  prmreclem1  14306  prmreclem5  14310  4sqlem10  14337  4sqlem12  14346  4sqlem16  14350  4sqlem17  14351  vdwlem3  14373  vdwlem8  14378  vdwlem9  14379  0ram  14410  ramz2  14414  xpsc0  14829  xpsc1  14830  odmulg  16447  dfod2  16455  odf1o1  16461  odf1o2  16462  sylow3lem4  16519  ablsub4  16692  odadd1  16723  odadd2  16724  ablfacrp2  16986  ablfac1b  16989  ablfac1eu  16992  pgpfac1lem3a  16995  pgpfaclem2  17001  chrcong  18433  znrrg  18471  cygznlem1  18472  chpdmatlem3  19208  txdis  19999  txdis1cn  20002  ptunhmeo  20175  qustgplem  20485  blcld  20874  nlmvscnlem2  21060  blcvx  21169  metds0  21220  metdseq0  21224  icopnfcnv  21308  lebnumii  21332  ipcau2  21543  tchcphlem1  21544  ipcnlem2  21550  csbren  21692  trirn  21693  dyadf  21866  dyadovol  21868  dyaddisjlem  21870  dyadmaxlem  21872  opnmbllem  21876  mbfmulc2lem  21920  mbfi1fseqlem4  21991  mbfi1fseqlem5  21992  mbfi1fseqlem6  21993  itg2mulclem  22019  itg2monolem1  22023  itg2monolem3  22025  itg2cnlem2  22035  itgabs  22107  dvlip  22260  dvlt0  22272  dvcvx  22287  ftc1lem4  22306  dgrcolem2  22536  aaliou3lem2  22604  aaliou3lem9  22611  itgulm  22668  radcnvlem1  22673  abelthlem2  22692  abelthlem7  22698  tangtx  22763  cosne0  22782  cosordlem  22783  tanord1  22789  logdivlti  22870  logcnlem4  22891  logf1o2  22896  cxpcn3lem  22986  cxpaddle  22991  ang180lem2  23007  atanlogsublem  23111  atantan  23119  atanbndlem  23121  atans2  23127  leibpi  23138  log2tlbnd  23141  birthdaylem3  23148  efrlim  23164  jensenlem2  23182  ftalem1  23211  ftalem5  23215  basellem1  23219  basellem4  23222  fsumdvdsdiaglem  23324  dvdsflf1o  23328  fsumfldivdiaglem  23330  ppiub  23344  mersenne  23367  dchrptlem1  23404  bposlem1  23424  bposlem2  23425  bposlem4  23427  lgsdilem  23462  lgseisenlem1  23489  lgseisenlem2  23490  lgseisenlem3  23491  lgsquadlem1  23494  lgsquadlem2  23495  2sqlem3  23506  2sqlem8  23512  2sqlem11  23515  2sqblem  23517  chebbnd1lem2  23520  chebbnd1lem3  23521  rplogsumlem1  23534  rplogsumlem2  23535  dchrisumlem1  23539  dchrmusum2  23544  dchrisum0flblem1  23558  mulog2sumlem1  23584  logdivbnd  23606  pntpbnd1a  23635  pntpbnd1  23636  pntpbnd2  23637  pntlemh  23649  pntlemr  23652  pntlemk  23656  pntlemo  23657  ostth2lem1  23668  ostth2lem2  23684  ostth2lem3  23685  ostth3  23688  legov  23837  axsegcon  24095  axpaschlem  24108  clwwlkf1  24661  vdgrun  24766  vdgrfiun  24767  eupath2lem3  24844  gxmodid  25146  nmbdoplbi  26808  nmcoplbi  26812  nmophmi  26815  nmbdfnlbi  26833  nmcfnlbi  26836  cnlnadjlem7  26857  nmopcoi  26879  resf1o  27418  xdivrec  27489  txomap  27703  unitdivcld  27749  measvunilem  28049  measvuni  28051  measssd  28052  measiuns  28054  measinblem  28057  measdivcst  28062  sibfof  28148  oddpwdc  28159  sseqfv1  28194  sseqfv2  28199  probun  28224  totprobd  28231  dstrvprob  28276  zetacvg  28423  subfaclim  28498  conpcon  28546  cvmliftlem2  28597  cvmliftlem6  28601  cvmliftlem7  28602  cvmliftlem8  28603  cvmliftlem9  28604  cvmliftlem10  28605  snmlff  28640  lineext  29694  hilbert1.1  29772  opnmbllem0  30018  ismblfin  30023  itgabsnc  30052  ftc1cnnclem  30056  nn0prpwlem  30108  bfplem1  30286  bfp  30288  eldioph2lem1  30661  fphpdo  30719  irrapxlem1  30726  irrapxlem2  30727  irrapxlem3  30728  irrapxlem5  30730  pellexlem2  30734  pell1234qrreccl  30758  pell1234qrmulcl  30759  pell1234qrdich  30765  pell1qr1  30775  pellqrexplicit  30781  pellfundex  30790  reglogltb  30795  reglogleb  30796  pellfund14  30802  rmspecsqrtnq  30810  rmxycomplete  30821  jm2.24nn  30865  jm2.17b  30867  jm2.17c  30868  jm2.18  30898  jm2.19lem2  30900  jm2.20nn  30907  jm2.16nn0  30914  jm3.1lem2  30928  areaquad  31153  stoweidlem1  31668  stoweidlem11  31678  stoweidlem14  31681  stoweidlem26  31693  stoweidlem34  31701  stoweidlem38  31705  stoweidlem60  31727  fourierdlem52  31826  domnmsuppn0  32672  lincvalpr  32729  ldepspr  32784  islindeps2  32794  lfl1  34497  lfladdcl  34498  eqlkr  34526  lkrlsp  34529  atcvrj2b  34858  3dim1  34893  3dim2  34894  llni2  34938  2llnjaN  34992  lvoli3  35003  lvoli2  35007  lncvrelatN  35207  lhpat4N  35470  lhpat3  35472  4atexlemex6  35500  ldilco  35542  ltrnid  35561  ltrnatb  35563  ltrnel  35565  ltrncnvel  35568  ltrncnv  35572  ltrn11at  35573  ltrneq  35575  ltrnmwOLD  35577  trlat  35596  trlator0  35598  ltrnnidn  35601  trlid0  35603  trlnidatb  35604  trlnle  35613  trlval3  35614  trlval4  35615  cdlemc2  35619  cdlemc5  35622  cdlemc6  35623  cdlemc  35624  cdlemd2  35626  cdlemd9  35633  cdleme0e  35644  cdleme02N  35649  cdleme0ex1N  35650  cdleme3e  35659  cdleme3g  35661  cdleme3h  35662  cdleme3  35664  cdleme7aa  35669  cdleme7b  35671  cdleme7c  35672  cdleme7d  35673  cdleme7e  35674  cdleme7ga  35675  cdleme7  35676  cdleme9  35680  cdleme16aN  35686  cdleme11c  35688  cdleme11dN  35689  cdleme11e  35690  cdleme11h  35693  cdleme11j  35694  cdleme11k  35695  cdleme12  35698  cdleme21j  35764  cdleme26eALTN  35789  cdleme26f  35791  cdleme26f2  35793  cdlemefrs29bpre0  35824  cdleme35a  35876  cdleme35b  35878  cdleme35c  35879  cdleme35f  35882  cdleme36a  35888  cdleme38m  35891  cdlemeg46rgv  35956  cdlemeg46req  35957  cdlemf  35991  cdlemg2fvlem  36022  cdlemg2l  36031  cdlemg7N  36054  cdlemg12g  36077  cdlemg15  36084  cdlemg17h  36096  cdlemg17  36105  cdlemg19a  36111  cdlemg24  36116  cdlemg37  36117  cdlemg27a  36120  cdlemg31b0N  36122  cdlemg27b  36124  cdlemg31c  36127  cdlemg31d  36128  cdlemg35  36141  trljco  36168  tgrpgrplem  36177  cdlemh2  36244  tendoconid  36257  tendotr  36258  cdlemk35s-id  36366  cdlemk39s-id  36368  cdlemk53b  36384  cdlemk53  36385  cdlemk54  36386  cdleml3N  36406  cdleml5N  36408  tendospcanN  36452  diclss  36622  dihvalcq2  36676  dihord4  36687  dihord5b  36688  dihord5apre  36691  dihmeetlem1N  36719  dihmeetbclemN  36733  dihmeetlem20N  36755  dihmeetALTN  36756  dihatlat  36763  dihatexv  36767  dochkr1  36907  dochkr1OLDN  36908  lcfl7lem  36928  lclkrlem2m  36948  hdmaplna1  37339  hdmaplns1  37340  hdmaplnm1  37341  lemuldiv3d  37594  lemuldiv4d  37595
  Copyright terms: Public domain W3C validator