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

Theorem syl112anc 1321
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 552 . 2 (𝜑 → (𝜃𝜏))
6 syl112anc.5 . 2 ((𝜓𝜒 ∧ (𝜃𝜏)) → 𝜂)
71, 2, 5, 6syl3anc 1317 1 (𝜑𝜂)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1030
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 195  df-an 384  df-3an 1032
This theorem is referenced by:  rmob2  3496  fveqf1o  6435  enfixsn  7931  gruina  9496  grur1  9498  enqeq  9612  recrec  10571  rec11r  10573  divdivdiv  10575  dmdcan  10584  ddcan  10588  rereccl  10592  div2neg  10597  divmuld  10672  divmul2d  10683  divmul3d  10684  divassd  10685  div12d  10686  div23d  10687  divdird  10688  divsubdird  10689  div11d  10690  ltmul12a  10728  ltdiv1  10736  ltrec  10754  lt2msq1  10756  lediv2  10762  supmul1  10839  qbtwnre  11863  xlemul1a  11947  xlemul1  11949  xadd4d  11962  quoremz  12471  quoremnn0ALT  12473  expgt1  12715  nnlesq  12785  expnbnd  12810  expmulnbnd  12813  discr1  12817  facubnd  12904  hashf1lem1  13048  2swrdeqwrdeq  13251  sqrlem6  13782  mulcn2  14120  climcnds  14368  geomulcvg  14392  cvgrat  14400  eftlub  14624  eflegeo  14636  tanhlt1  14675  sin01bnd  14700  cos01bnd  14701  eirrlem  14717  bitsmod  14942  mulgcd  15049  mulgcddvds  15153  prmind2  15182  qnumgt0  15242  iserodd  15324  pcpremul  15332  fldivp1  15385  pcfaclem  15386  qexpz  15389  prmpwdvds  15392  pockthg  15394  prmreclem1  15404  prmreclem5  15408  4sqlem10  15435  4sqlem12  15444  4sqlem16  15448  4sqlem17  15449  vdwlem3  15471  vdwlem8  15476  vdwlem9  15477  0ram  15508  ramz2  15512  xpsc0  15989  xpsc1  15990  odmulg  17742  dfod2  17750  odf1o1  17756  odf1o2  17757  sylow3lem4  17814  ablsub4  17987  odadd1  18020  odadd2  18021  ablfacrp2  18235  ablfac1b  18238  ablfac1eu  18241  pgpfac1lem3a  18244  pgpfaclem2  18250  chrcong  19641  znrrg  19678  cygznlem1  19679  chpdmatlem3  20406  txdis  21187  txdis1cn  21190  ptunhmeo  21363  qustgplem  21676  blcld  22061  nlmvscnlem2  22232  blcvx  22341  metds0  22392  metdseq0  22396  icopnfcnv  22480  lebnumii  22504  ipcau2  22762  tchcphlem1  22763  ipcnlem2  22769  csbren  22907  trirn  22908  dyadf  23082  dyadovol  23084  dyaddisjlem  23086  dyadmaxlem  23088  opnmbllem  23092  mbfmulc2lem  23137  mbfi1fseqlem4  23208  mbfi1fseqlem5  23209  mbfi1fseqlem6  23210  itg2mulclem  23236  itg2monolem1  23240  itg2monolem3  23242  itg2cnlem2  23252  itgabs  23324  dvlip  23477  dvlt0  23489  dvcvx  23504  ftc1lem4  23523  dgrcolem2  23751  aaliou3lem2  23819  aaliou3lem9  23826  itgulm  23883  radcnvlem1  23888  abelthlem2  23907  abelthlem7  23913  tangtx  23978  cosne0  23997  cosordlem  23998  tanord1  24004  logdivlti  24087  logcnlem4  24108  logf1o2  24113  cxpcn3lem  24205  cxpaddle  24210  ang180lem2  24257  atanlogsublem  24359  atantan  24367  atanbndlem  24369  atans2  24375  leibpi  24386  log2tlbnd  24389  birthdaylem3  24397  efrlim  24413  jensenlem2  24431  zetacvg  24458  ftalem1  24516  ftalem5  24520  basellem1  24524  basellem4  24527  fsumdvdsdiaglem  24626  dvdsflf1o  24630  fsumfldivdiaglem  24632  ppiub  24646  mersenne  24669  dchrptlem1  24706  bposlem1  24726  bposlem2  24727  bposlem4  24729  lgsdilem  24766  lgseisenlem1  24817  lgseisenlem2  24818  lgseisenlem3  24819  lgsquadlem1  24822  lgsquadlem2  24823  2sqlem3  24862  2sqlem8  24868  2sqlem11  24871  2sqblem  24873  chebbnd1lem2  24876  chebbnd1lem3  24877  rplogsumlem1  24890  rplogsumlem2  24891  dchrisumlem1  24895  dchrmusum2  24900  dchrisum0flblem1  24914  mulog2sumlem1  24940  logdivbnd  24962  pntpbnd1a  24991  pntpbnd1  24992  pntpbnd2  24993  pntlemh  25005  pntlemr  25008  pntlemk  25012  pntlemo  25013  ostth2lem1  25024  ostth2lem2  25040  ostth2lem3  25041  ostth3  25044  legov  25198  axsegcon  25525  axpaschlem  25538  clwwlkf1  26090  vdgrun  26194  vdgrfiun  26195  eupath2lem3  26272  nmblolbii  26844  nmbdoplbi  28073  nmcoplbi  28077  nmophmi  28080  nmbdfnlbi  28098  nmcfnlbi  28101  cnlnadjlem7  28122  nmopcoi  28144  resf1o  28699  xdivrec  28772  txomap  29035  unitdivcld  29081  measvunilem  29408  measvuni  29410  measssd  29411  measiuns  29413  measinblem  29416  measdivcst  29421  sibfof  29535  oddpwdc  29549  sseqfv1  29584  sseqfv2  29589  probun  29614  totprobd  29621  dstrvprob  29666  subfaclim  30230  conpcon  30277  cvmliftlem2  30328  cvmliftlem6  30332  cvmliftlem7  30333  cvmliftlem8  30334  cvmliftlem9  30335  cvmliftlem10  30336  snmlff  30371  lineext  31159  hilbert1.1  31237  nn0prpwlem  31293  poimirlem1  32376  opnmbllem0  32411  ismblfin  32416  itgabsnc  32445  ftc1cnnclem  32449  bfplem1  32587  bfp  32589  lfl1  33171  lfladdcl  33172  eqlkr  33200  lkrlsp  33203  atcvrj2b  33532  3dim1  33567  3dim2  33568  llni2  33612  2llnjaN  33666  lvoli3  33677  lvoli2  33681  lncvrelatN  33881  lhpat4N  34144  lhpat3  34146  4atexlemex6  34174  ldilco  34216  ltrnid  34235  ltrnatb  34237  ltrnel  34239  ltrncnvel  34242  ltrncnv  34246  ltrn11at  34247  ltrneq  34249  ltrnmwOLD  34252  trlat  34270  trlator0  34272  ltrnnidn  34275  trlid0  34277  trlnidatb  34278  trlnle  34287  trlval3  34288  trlval4  34289  cdlemc2  34293  cdlemc5  34296  cdlemc6  34297  cdlemc  34298  cdlemd2  34300  cdlemd9  34307  cdleme0e  34318  cdleme02N  34323  cdleme0ex1N  34324  cdleme3e  34333  cdleme3g  34335  cdleme3h  34336  cdleme3  34338  cdleme7aa  34343  cdleme7b  34345  cdleme7c  34346  cdleme7d  34347  cdleme7e  34348  cdleme7ga  34349  cdleme7  34350  cdleme9  34354  cdleme16aN  34360  cdleme11c  34362  cdleme11dN  34363  cdleme11e  34364  cdleme11h  34367  cdleme11j  34368  cdleme11k  34369  cdleme12  34372  cdleme21j  34438  cdleme26eALTN  34463  cdleme26f  34465  cdleme26f2  34467  cdlemefrs29bpre0  34498  cdleme35a  34550  cdleme35b  34552  cdleme35c  34553  cdleme35f  34556  cdleme36a  34562  cdleme38m  34565  cdlemeg46rgv  34630  cdlemeg46req  34631  cdlemf  34665  cdlemg2fvlem  34696  cdlemg2l  34705  cdlemg7N  34728  cdlemg12g  34751  cdlemg15  34758  cdlemg17h  34770  cdlemg17  34779  cdlemg19a  34785  cdlemg24  34790  cdlemg37  34791  cdlemg27a  34794  cdlemg31b0N  34796  cdlemg27b  34798  cdlemg31c  34801  cdlemg31d  34802  cdlemg35  34815  trljco  34842  tgrpgrplem  34851  cdlemh2  34918  tendoconid  34931  tendotr  34932  cdlemk35s-id  35040  cdlemk39s-id  35042  cdlemk53b  35058  cdlemk53  35059  cdlemk54  35060  cdleml3N  35080  cdleml5N  35082  tendospcanN  35126  diclss  35296  dihvalcq2  35350  dihord4  35361  dihord5b  35362  dihord5apre  35365  dihmeetlem1N  35393  dihmeetbclemN  35407  dihmeetlem20N  35429  dihmeetALTN  35430  dihatlat  35437  dihatexv  35441  dochkr1  35581  dochkr1OLDN  35582  lcfl7lem  35602  lclkrlem2m  35622  hdmaplna1  36013  hdmaplns1  36014  hdmaplnm1  36015  eldioph2lem1  36137  fphpdo  36195  irrapxlem1  36200  irrapxlem2  36201  irrapxlem3  36202  irrapxlem5  36204  pellexlem2  36208  pell1234qrreccl  36232  pell1234qrmulcl  36233  pell1234qrdich  36239  pell1qr1  36249  pellqrexplicit  36255  pellfundex  36264  reglogltb  36269  reglogleb  36270  pellfund14  36276  rmspecsqrtnqOLD  36285  rmxycomplete  36296  jm2.24nn  36340  jm2.17b  36342  jm2.17c  36343  jm2.18  36369  jm2.19lem2  36371  jm2.20nn  36378  jm2.16nn0  36385  jm3.1lem2  36399  areaquad  36617  clsk3nimkb  37154  lemuldiv3d  37290  lemuldiv4d  37291  stoweidlem1  38691  stoweidlem11  38701  stoweidlem14  38704  stoweidlem26  38716  stoweidlem34  38724  stoweidlem38  38728  stoweidlem60  38750  fourierdlem52  38848  etransclem38  38962  pfxsuffeqwrdeq  40067  0uhgrsubgr  40498  clwwlksf1  41219  upgr4cycl4dv4e  41347  eupth2lem3lem3  41393  domnmsuppn0  41939  lincvalpr  41996  ldepspr  42051  islindeps2  42061  fldivexpfllog2  42152
  Copyright terms: Public domain W3C validator