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

Theorem syl112anc 1486
Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
Hypotheses
Ref Expression
syl3anc.1 (𝜑𝜓)
syl3anc.2 (𝜑𝜒)
syl3anc.3 (𝜑𝜃)
syl3Xanc.4 (𝜑𝜏)
syl112anc.5 ((𝜓𝜒 ∧ (𝜃𝜏)) → 𝜂)
Assertion
Ref Expression
syl112anc (𝜑𝜂)

Proof of Theorem syl112anc
StepHypRef Expression
1 syl3anc.1 . 2 (𝜑𝜓)
2 syl3anc.2 . 2 (𝜑𝜒)
3 syl3anc.3 . . 3 (𝜑𝜃)
4 syl3Xanc.4 . . 3 (𝜑𝜏)
53, 4jca 503 . 2 (𝜑 → (𝜃𝜏))
6 syl112anc.5 . 2 ((𝜓𝜒 ∧ (𝜃𝜏)) → 𝜂)
71, 2, 5, 6syl3anc 1483 1 (𝜑𝜂)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1100
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 198  df-an 385  df-3an 1102
This theorem is referenced by:  rmob2  3733  fveqf1o  6784  enfixsn  8311  gruina  9928  grur1  9930  enqeq  10044  recrec  11010  rec11r  11012  divdivdiv  11014  dmdcan  11023  ddcan  11027  rereccl  11031  div2neg  11036  divmuld  11111  divmul2d  11122  divmul3d  11123  divassd  11124  div12d  11125  div23d  11126  divdird  11127  divsubdird  11128  div11d  11129  ltmul12a  11167  ltdiv1  11175  ltrec  11193  lt2msq1  11195  lediv2  11201  supmul1  11280  qbtwnre  12251  xlemul1a  12339  xlemul1  12341  xadd4d  12354  quoremz  12881  quoremnn0ALT  12883  expgt1  13124  nnlesq  13194  expnbnd  13219  expmulnbnd  13222  discr1  13226  facubnd  13310  hashf1lem1  13459  2swrdeqwrdeq  13680  sqrlem6  14214  mulcn2  14552  geomulcvg  14832  cvgrat  14839  eftlub  15062  eflegeo  15074  tanhlt1  15113  sin01bnd  15138  cos01bnd  15139  eirrlem  15155  bitsmod  15380  mulgcd  15487  mulgcddvds  15590  prmind2  15619  qnumgt0  15678  pcpremul  15768  fldivp1  15821  pcfaclem  15822  qexpz  15825  prmpwdvds  15828  pockthg  15830  prmreclem1  15840  prmreclem5  15844  4sqlem10  15871  4sqlem12  15880  4sqlem16  15884  4sqlem17  15885  vdwlem3  15907  vdwlem8  15912  vdwlem9  15913  0ram  15944  ramz2  15948  xpsc0  16428  xpsc1  16429  odmulg  18177  dfod2  18185  odf1o1  18191  odf1o2  18192  sylow3lem4  18249  ablsub4  18422  odadd1  18455  odadd2  18456  ablfacrp2  18671  ablfac1b  18674  ablfac1eu  18677  pgpfac1lem3a  18680  pgpfaclem2  18686  chrcong  20088  znrrg  20124  cygznlem1  20125  chpdmatlem3  20862  txdis  21653  txdis1cn  21656  ptunhmeo  21829  qustgplem  22141  blcld  22527  nlmvscnlem2  22706  blcvx  22818  metds0  22870  metdseq0  22874  icopnfcnv  22958  lebnumii  22982  ipcau2  23249  tchcphlem1  23250  ipcnlem2  23259  csbren  23400  trirn  23401  dyadf  23578  dyadovol  23580  dyaddisjlem  23582  dyadmaxlem  23584  opnmbllem  23588  mbfmulc2lem  23634  mbfi1fseqlem4  23705  mbfi1fseqlem5  23706  mbfi1fseqlem6  23707  itg2mulclem  23733  itg2monolem1  23737  itg2monolem3  23739  itg2cnlem2  23749  itgabs  23821  dvlip  23976  dvlt0  23988  dvcvx  24003  ftc1lem4  24022  dgrcolem2  24250  aaliou3lem2  24318  aaliou3lem9  24325  itgulm  24382  radcnvlem1  24387  abelthlem2  24406  abelthlem7  24412  tangtx  24478  cosne0  24497  cosordlem  24498  tanord1  24504  logdivlti  24586  logcnlem4  24611  logf1o2  24616  cxpcn3lem  24708  cxpaddle  24713  ang180lem2  24760  atanlogsublem  24862  atantan  24870  atanbndlem  24872  atans2  24878  leibpi  24889  log2tlbnd  24892  birthdaylem3  24900  efrlim  24916  jensenlem2  24934  zetacvg  24961  ftalem1  25019  ftalem5  25023  basellem1  25027  basellem4  25030  fsumdvdsdiaglem  25129  dvdsflf1o  25133  fsumfldivdiaglem  25135  ppiub  25149  mersenne  25172  dchrptlem1  25209  bposlem1  25229  bposlem2  25230  bposlem4  25232  lgsdilem  25269  lgseisenlem1  25320  lgseisenlem2  25321  lgseisenlem3  25322  lgsquadlem1  25325  lgsquadlem2  25326  2sqlem3  25365  2sqlem8  25371  2sqlem11  25374  2sqblem  25376  chebbnd1lem2  25379  chebbnd1lem3  25380  rplogsumlem1  25393  rplogsumlem2  25394  dchrisumlem1  25398  dchrmusum2  25403  dchrisum0flblem1  25417  mulog2sumlem1  25443  logdivbnd  25465  pntpbnd1a  25494  pntpbnd1  25495  pntpbnd2  25496  pntlemh  25508  pntlemr  25511  pntlemk  25515  pntlemo  25516  ostth2lem1  25527  ostth2lem2  25543  ostth2lem3  25544  ostth3  25547  legov  25700  axsegcon  26027  axpaschlem  26040  0uhgrsubgr  26393  clwwlkf1  27204  upgr4cycl4dv4e  27364  eupth2lem3lem3  27409  nmblolbii  27988  nmbdoplbi  29217  nmcoplbi  29221  nmophmi  29224  nmbdfnlbi  29242  nmcfnlbi  29245  cnlnadjlem7  29266  nmopcoi  29288  resf1o  29838  xdivrec  29966  txomap  30232  unitdivcld  30278  measvunilem  30606  measvuni  30608  measssd  30609  measiuns  30611  measinblem  30614  measdivcst  30619  sibfof  30733  oddpwdc  30747  sseqfv1  30782  sseqfv2  30787  probun  30812  totprobd  30819  dstrvprob  30864  actfunsnrndisj  31014  reprsuc  31024  breprexplema  31039  subfaclim  31498  connpconn  31545  cvmliftlem2  31596  cvmliftlem6  31600  cvmliftlem7  31601  cvmliftlem8  31602  cvmliftlem9  31603  cvmliftlem10  31604  snmlff  31639  noextenddif  32147  noextendlt  32148  noextendgt  32149  nosupbnd1lem3  32182  nosupbnd1lem4  32183  nosupbnd1lem5  32184  nosupbnd1lem6  32185  noetalem3  32191  lineext  32509  hilbert1.1  32587  nn0prpwlem  32643  poimirlem1  33725  opnmbllem0  33760  ismblfin  33765  itgabsnc  33793  ftc1cnnclem  33797  bfplem1  33934  bfp  33936  lfl1  34852  lfladdcl  34853  eqlkr  34881  lkrlsp  34884  atcvrj2b  35214  3dim1  35249  3dim2  35250  llni2  35294  2llnjaN  35348  lvoli3  35359  lvoli2  35363  lncvrelatN  35563  lhpat4N  35826  lhpat3  35828  4atexlemex6  35856  ldilco  35898  ltrnid  35917  ltrnatb  35919  ltrnel  35921  ltrncnvel  35924  ltrncnv  35928  ltrn11at  35929  ltrneq  35931  trlat  35951  trlator0  35953  ltrnnidn  35956  trlid0  35958  trlnidatb  35959  trlnle  35968  trlval3  35969  trlval4  35970  cdlemc2  35974  cdlemc5  35977  cdlemc6  35978  cdlemc  35979  cdlemd2  35981  cdlemd9  35988  cdleme0e  35999  cdleme02N  36004  cdleme0ex1N  36005  cdleme3e  36014  cdleme3g  36016  cdleme3h  36017  cdleme3  36019  cdleme7aa  36024  cdleme7b  36026  cdleme7c  36027  cdleme7d  36028  cdleme7e  36029  cdleme7ga  36030  cdleme7  36031  cdleme9  36035  cdleme16aN  36041  cdleme11c  36043  cdleme11dN  36044  cdleme11e  36045  cdleme11h  36048  cdleme11j  36049  cdleme11k  36050  cdleme12  36053  cdleme21j  36118  cdleme26eALTN  36143  cdleme26f  36145  cdleme26f2  36147  cdlemefrs29bpre0  36178  cdleme35a  36230  cdleme35b  36232  cdleme35c  36233  cdleme35f  36236  cdleme36a  36242  cdleme38m  36245  cdlemeg46rgv  36310  cdlemeg46req  36311  cdlemf  36345  cdlemg2fvlem  36376  cdlemg2l  36385  cdlemg7N  36408  cdlemg12g  36431  cdlemg15  36438  cdlemg17h  36450  cdlemg17  36459  cdlemg19a  36465  cdlemg24  36470  cdlemg37  36471  cdlemg27a  36474  cdlemg31b0N  36476  cdlemg27b  36478  cdlemg31c  36481  cdlemg31d  36482  cdlemg35  36495  trljco  36522  tgrpgrplem  36531  cdlemh2  36598  tendoconid  36611  tendotr  36612  cdlemk35s-id  36720  cdlemk39s-id  36722  cdlemk53b  36738  cdlemk53  36739  cdlemk54  36740  cdleml3N  36760  cdleml5N  36762  tendospcanN  36805  diclss  36975  dihvalcq2  37029  dihord4  37040  dihord5b  37041  dihord5apre  37044  dihmeetlem1N  37072  dihmeetbclemN  37086  dihmeetlem20N  37108  dihmeetALTN  37109  dihatlat  37116  dihatexv  37120  dochkr1  37260  dochkr1OLDN  37261  lcfl7lem  37281  lclkrlem2m  37301  hdmaplna1  37689  hdmaplns1  37690  hdmaplnm1  37691  eldioph2lem1  37826  fphpdo  37884  irrapxlem1  37889  irrapxlem2  37890  irrapxlem3  37891  irrapxlem5  37893  pellexlem2  37897  pell1234qrreccl  37921  pell1234qrmulcl  37922  pell1234qrdich  37928  pell1qr1  37938  pellqrexplicit  37944  pellfundex  37953  reglogltb  37958  reglogleb  37959  pellfund14  37965  rmxycomplete  37984  jm2.24nn  38028  jm2.17b  38030  jm2.17c  38031  jm2.18  38057  jm2.19lem2  38059  jm2.20nn  38066  jm2.16nn0  38073  jm3.1lem2  38087  areaquad  38303  clsk3nimkb  38839  lemuldiv3d  38973  lemuldiv4d  38974  stoweidlem1  40698  stoweidlem11  40708  stoweidlem14  40711  stoweidlem26  40723  stoweidlem34  40731  stoweidlem38  40735  stoweidlem60  40757  fourierdlem52  40855  etransclem38  40969  pfxsuffeqwrdeq  41982  domnmsuppn0  42719  lincvalpr  42776  ldepspr  42831  islindeps2  42841  fldivexpfllog2  42928
  Copyright terms: Public domain W3C validator