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

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

Proof of Theorem syl112anc
StepHypRef Expression
1 syl12anc.1 . 2 (𝜑𝜓)
2 syl12anc.2 . 2 (𝜑𝜒)
3 syl12anc.3 . . 3 (𝜑𝜃)
4 syl22anc.4 . . 3 (𝜑𝜏)
53, 4jca 555 . 2 (𝜑 → (𝜃𝜏))
6 syl112anc.5 . 2 ((𝜓𝜒 ∧ (𝜃𝜏)) → 𝜂)
71, 2, 5, 6syl3anc 1463 1 (𝜑𝜂)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1072
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 197  df-an 385  df-3an 1074
This theorem is referenced by:  rmob2  3660  fveqf1o  6708  enfixsn  8222  gruina  9803  grur1  9805  enqeq  9919  recrec  10885  rec11r  10887  divdivdiv  10889  dmdcan  10898  ddcan  10902  rereccl  10906  div2neg  10911  divmuld  10986  divmul2d  10997  divmul3d  10998  divassd  10999  div12d  11000  div23d  11001  divdird  11002  divsubdird  11003  div11d  11004  ltmul12a  11042  ltdiv1  11050  ltrec  11068  lt2msq1  11070  lediv2  11076  supmul1  11155  qbtwnre  12194  xlemul1a  12282  xlemul1  12284  xadd4d  12297  quoremz  12819  quoremnn0ALT  12821  expgt1  13063  nnlesq  13133  expnbnd  13158  expmulnbnd  13161  discr1  13165  facubnd  13252  hashf1lem1  13402  2swrdeqwrdeq  13624  sqrlem6  14158  mulcn2  14496  climcnds  14753  geomulcvg  14777  cvgrat  14785  eftlub  15009  eflegeo  15021  tanhlt1  15060  sin01bnd  15085  cos01bnd  15086  eirrlem  15102  bitsmod  15331  mulgcd  15438  mulgcddvds  15542  prmind2  15571  qnumgt0  15631  iserodd  15713  pcpremul  15721  fldivp1  15774  pcfaclem  15775  qexpz  15778  prmpwdvds  15781  pockthg  15783  prmreclem1  15793  prmreclem5  15797  4sqlem10  15824  4sqlem12  15833  4sqlem16  15837  4sqlem17  15838  vdwlem3  15860  vdwlem8  15865  vdwlem9  15866  0ram  15897  ramz2  15901  xpsc0  16393  xpsc1  16394  odmulg  18144  dfod2  18152  odf1o1  18158  odf1o2  18159  sylow3lem4  18216  ablsub4  18389  odadd1  18422  odadd2  18423  ablfacrp2  18637  ablfac1b  18640  ablfac1eu  18643  pgpfac1lem3a  18646  pgpfaclem2  18652  chrcong  20050  znrrg  20087  cygznlem1  20088  chpdmatlem3  20818  txdis  21608  txdis1cn  21611  ptunhmeo  21784  qustgplem  22096  blcld  22482  nlmvscnlem2  22661  blcvx  22773  metds0  22825  metdseq0  22829  icopnfcnv  22913  lebnumii  22937  ipcau2  23204  tchcphlem1  23205  ipcnlem2  23214  csbren  23353  trirn  23354  dyadf  23530  dyadovol  23532  dyaddisjlem  23534  dyadmaxlem  23536  opnmbllem  23540  mbfmulc2lem  23584  mbfi1fseqlem4  23655  mbfi1fseqlem5  23656  mbfi1fseqlem6  23657  itg2mulclem  23683  itg2monolem1  23687  itg2monolem3  23689  itg2cnlem2  23699  itgabs  23771  dvlip  23926  dvlt0  23938  dvcvx  23953  ftc1lem4  23972  dgrcolem2  24200  aaliou3lem2  24268  aaliou3lem9  24275  itgulm  24332  radcnvlem1  24337  abelthlem2  24356  abelthlem7  24362  tangtx  24427  cosne0  24446  cosordlem  24447  tanord1  24453  logdivlti  24536  logcnlem4  24561  logf1o2  24566  cxpcn3lem  24658  cxpaddle  24663  ang180lem2  24710  atanlogsublem  24812  atantan  24820  atanbndlem  24822  atans2  24828  leibpi  24839  log2tlbnd  24842  birthdaylem3  24850  efrlim  24866  jensenlem2  24884  zetacvg  24911  ftalem1  24969  ftalem5  24973  basellem1  24977  basellem4  24980  fsumdvdsdiaglem  25079  dvdsflf1o  25083  fsumfldivdiaglem  25085  ppiub  25099  mersenne  25122  dchrptlem1  25159  bposlem1  25179  bposlem2  25180  bposlem4  25182  lgsdilem  25219  lgseisenlem1  25270  lgseisenlem2  25271  lgseisenlem3  25272  lgsquadlem1  25275  lgsquadlem2  25276  2sqlem3  25315  2sqlem8  25321  2sqlem11  25324  2sqblem  25326  chebbnd1lem2  25329  chebbnd1lem3  25330  rplogsumlem1  25343  rplogsumlem2  25344  dchrisumlem1  25348  dchrmusum2  25353  dchrisum0flblem1  25367  mulog2sumlem1  25393  logdivbnd  25415  pntpbnd1a  25444  pntpbnd1  25445  pntpbnd2  25446  pntlemh  25458  pntlemr  25461  pntlemk  25465  pntlemo  25466  ostth2lem1  25477  ostth2lem2  25493  ostth2lem3  25494  ostth3  25497  legov  25650  axsegcon  25977  axpaschlem  25990  0uhgrsubgr  26341  clwwlkf1  27149  upgr4cycl4dv4e  27308  eupth2lem3lem3  27353  nmblolbii  27934  nmbdoplbi  29163  nmcoplbi  29167  nmophmi  29170  nmbdfnlbi  29188  nmcfnlbi  29191  cnlnadjlem7  29212  nmopcoi  29234  resf1o  29785  xdivrec  29915  txomap  30181  unitdivcld  30227  measvunilem  30555  measvuni  30557  measssd  30558  measiuns  30560  measinblem  30563  measdivcst  30568  sibfof  30682  oddpwdc  30696  sseqfv1  30731  sseqfv2  30736  probun  30761  totprobd  30768  dstrvprob  30813  actfunsnrndisj  30963  reprsuc  30973  breprexplema  30988  subfaclim  31448  connpconn  31495  cvmliftlem2  31546  cvmliftlem6  31550  cvmliftlem7  31551  cvmliftlem8  31552  cvmliftlem9  31553  cvmliftlem10  31554  snmlff  31589  noextenddif  32098  noextendlt  32099  noextendgt  32100  nosupbnd1lem3  32133  nosupbnd1lem4  32134  nosupbnd1lem5  32135  nosupbnd1lem6  32136  noetalem3  32142  lineext  32460  hilbert1.1  32538  nn0prpwlem  32594  poimirlem1  33692  opnmbllem0  33727  ismblfin  33732  itgabsnc  33761  ftc1cnnclem  33765  bfplem1  33903  bfp  33905  lfl1  34829  lfladdcl  34830  eqlkr  34858  lkrlsp  34861  atcvrj2b  35190  3dim1  35225  3dim2  35226  llni2  35270  2llnjaN  35324  lvoli3  35335  lvoli2  35339  lncvrelatN  35539  lhpat4N  35802  lhpat3  35804  4atexlemex6  35832  ldilco  35874  ltrnid  35893  ltrnatb  35895  ltrnel  35897  ltrncnvel  35900  ltrncnv  35904  ltrn11at  35905  ltrneq  35907  ltrnmwOLD  35910  trlat  35928  trlator0  35930  ltrnnidn  35933  trlid0  35935  trlnidatb  35936  trlnle  35945  trlval3  35946  trlval4  35947  cdlemc2  35951  cdlemc5  35954  cdlemc6  35955  cdlemc  35956  cdlemd2  35958  cdlemd9  35965  cdleme0e  35976  cdleme02N  35981  cdleme0ex1N  35982  cdleme3e  35991  cdleme3g  35993  cdleme3h  35994  cdleme3  35996  cdleme7aa  36001  cdleme7b  36003  cdleme7c  36004  cdleme7d  36005  cdleme7e  36006  cdleme7ga  36007  cdleme7  36008  cdleme9  36012  cdleme16aN  36018  cdleme11c  36020  cdleme11dN  36021  cdleme11e  36022  cdleme11h  36025  cdleme11j  36026  cdleme11k  36027  cdleme12  36030  cdleme21j  36095  cdleme26eALTN  36120  cdleme26f  36122  cdleme26f2  36124  cdlemefrs29bpre0  36155  cdleme35a  36207  cdleme35b  36209  cdleme35c  36210  cdleme35f  36213  cdleme36a  36219  cdleme38m  36222  cdlemeg46rgv  36287  cdlemeg46req  36288  cdlemf  36322  cdlemg2fvlem  36353  cdlemg2l  36362  cdlemg7N  36385  cdlemg12g  36408  cdlemg15  36415  cdlemg17h  36427  cdlemg17  36436  cdlemg19a  36442  cdlemg24  36447  cdlemg37  36448  cdlemg27a  36451  cdlemg31b0N  36453  cdlemg27b  36455  cdlemg31c  36458  cdlemg31d  36459  cdlemg35  36472  trljco  36499  tgrpgrplem  36508  cdlemh2  36575  tendoconid  36588  tendotr  36589  cdlemk35s-id  36697  cdlemk39s-id  36699  cdlemk53b  36715  cdlemk53  36716  cdlemk54  36717  cdleml3N  36737  cdleml5N  36739  tendospcanN  36783  diclss  36953  dihvalcq2  37007  dihord4  37018  dihord5b  37019  dihord5apre  37022  dihmeetlem1N  37050  dihmeetbclemN  37064  dihmeetlem20N  37086  dihmeetALTN  37087  dihatlat  37094  dihatexv  37098  dochkr1  37238  dochkr1OLDN  37239  lcfl7lem  37259  lclkrlem2m  37279  hdmaplna1  37670  hdmaplns1  37671  hdmaplnm1  37672  eldioph2lem1  37794  fphpdo  37852  irrapxlem1  37857  irrapxlem2  37858  irrapxlem3  37859  irrapxlem5  37861  pellexlem2  37865  pell1234qrreccl  37889  pell1234qrmulcl  37890  pell1234qrdich  37896  pell1qr1  37906  pellqrexplicit  37912  pellfundex  37921  reglogltb  37926  reglogleb  37927  pellfund14  37933  rmspecsqrtnqOLD  37942  rmxycomplete  37953  jm2.24nn  37997  jm2.17b  37999  jm2.17c  38000  jm2.18  38026  jm2.19lem2  38028  jm2.20nn  38035  jm2.16nn0  38042  jm3.1lem2  38056  areaquad  38273  clsk3nimkb  38809  lemuldiv3d  38943  lemuldiv4d  38944  stoweidlem1  40690  stoweidlem11  40700  stoweidlem14  40703  stoweidlem26  40715  stoweidlem34  40723  stoweidlem38  40727  stoweidlem60  40749  fourierdlem52  40847  etransclem38  40961  pfxsuffeqwrdeq  41885  domnmsuppn0  42629  lincvalpr  42686  ldepspr  42741  islindeps2  42751  fldivexpfllog2  42838
  Copyright terms: Public domain W3C validator