Theorem syl112anc 1376

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

Step	Hyp	Ref	Expression
1		syl3anc.1	. 2 ⊢ (𝜑 → 𝜓)
2		syl3anc.2	. 2 ⊢ (𝜑 → 𝜒)
3		syl3anc.3	. . 3 ⊢ (𝜑 → 𝜃)
4		syl3Xanc.4	. . 3 ⊢ (𝜑 → 𝜏)
5	3, 4	jca 511	. 2 ⊢ (𝜑 → (𝜃 ∧ 𝜏))
6		syl112anc.5	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ (𝜃 ∧ 𝜏)) → 𝜂)
7	1, 2, 5, 6	syl3anc 1373	1 ⊢ (𝜑 → 𝜂)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  rmob2  3855  2nreu  4407  fveqf1o  7277  frrlem12  8276  enfixsn  9050  gruina  10771  grur1  10773  enqeq  10887  recrec  11879  rec11r  11881  divdivdiv  11883  dmdcan  11892  ddcan  11896  rereccl  11900  div2neg  11905  divmuld  11980  divmul2d  11991  divmul3d  11992  divassd  11993  div12d  11994  div23d  11995  divdird  11996  divsubdird  11997  div11d  11998  ltmul12a  12038  ltdiv1  12047  ltrec  12065  lt2msq1  12067  lediv2  12073  supmul1  12152  qbtwnre  13159  xlemul1a  13248  xlemul1  13250  xadd4d  13263  quoremz  13817  quoremnn0ALT  13819  expgt1  14065  nnlesq  14170  expnbnd  14197  expmulnbnd  14200  discr1  14204  facubnd  14265  pfxsuffeqwrdeq  14663  01sqrexlem6  15213  mulcn2  15562  geomulcvg  15842  cvgrat  15849  eftlub  16077  eflegeo  16089  tanhlt1  16128  sin01bnd  16153  cos01bnd  16154  eirrlem  16172  bitsmod  16406  mulgcd  16518  mulgcddvds  16625  prmind2  16655  qnumgt0  16720  pcpremul  16814  fldivp1  16868  pcfaclem  16869  qexpz  16872  prmpwdvds  16875  pockthg  16877  prmreclem1  16887  prmreclem5  16891  4sqlem10  16918  4sqlem12  16927  4sqlem16  16931  4sqlem17  16932  vdwlem3  16954  vdwlem8  16959  vdwlem9  16960  0ram  16991  ramz2  16995  cat1lem  18058  odmulg  19486  dfod2  19494  odf1o1  19502  odf1o2  19503  sylow3lem4  19560  ablsub4  19740  odadd1  19778  odadd2  19779  ablfacrp2  19999  ablfac1b  20002  ablfac1eu  20005  pgpfac1lem3a  20008  pgpfaclem2  20014  ablsimpgfindlem1  20039  chrcong  21437  znrrg  21475  cygznlem1  21476  chpdmatlem3  22727  txdis  23519  txdis1cn  23522  ptunhmeo  23695  qustgplem  24008  blcld  24393  nlmvscnlem2  24573  blcvx  24686  metds0  24739  metdseq0  24743  icopnfcnv  24840  lebnumii  24865  ipcau2  25134  tcphcphlem1  25135  ipcnlem2  25144  csbren  25299  trirn  25300  dyadf  25492  dyadovol  25494  dyaddisjlem  25496  dyadmaxlem  25498  opnmbllem  25502  mbfmulc2lem  25548  mbfi1fseqlem4  25619  mbfi1fseqlem5  25620  mbfi1fseqlem6  25621  itg2mulclem  25647  itg2monolem1  25651  itg2monolem3  25653  itg2cnlem2  25663  itgabs  25736  dvlip  25898  dvlt0  25910  dvcvx  25925  ftc1lem4  25946  dgrcolem2  26180  aaliou3lem2  26251  aaliou3lem9  26258  itgulm  26317  radcnvlem1  26322  abelthlem2  26342  abelthlem7  26348  tangtx  26414  cosne0  26438  cosordlem  26439  tanord1  26446  logdivlti  26529  logcnlem4  26554  logf1o2  26559  cxpcn3lem  26657  cxpaddle  26662  ang180lem2  26720  atanlogsublem  26825  atantan  26833  atanbndlem  26835  atans2  26841  leibpi  26852  log2tlbnd  26855  birthdaylem3  26863  efrlim  26879  efrlimOLD  26880  jensenlem2  26898  zetacvg  26925  ftalem1  26983  ftalem5  26987  basellem1  26991  basellem4  26994  fsumdvdsdiaglem  27093  dvdsflf1o  27097  fsumfldivdiaglem  27099  ppiub  27115  mersenne  27138  dchrptlem1  27175  bposlem1  27195  bposlem2  27196  bposlem4  27198  lgsdilem  27235  lgseisenlem1  27286  lgseisenlem2  27287  lgseisenlem3  27288  lgsquadlem1  27291  lgsquadlem2  27292  2sqlem3  27331  2sqlem8  27337  2sqlem11  27340  2sqblem  27342  chebbnd1lem2  27381  chebbnd1lem3  27382  rplogsumlem1  27395  rplogsumlem2  27396  dchrisumlem1  27400  dchrmusum2  27405  dchrisum0flblem1  27419  mulog2sumlem1  27445  logdivbnd  27467  pntpbnd1a  27496  pntpbnd1  27497  pntpbnd2  27498  pntlemh  27510  pntlemr  27513  pntlemk  27517  pntlemo  27518  ostth2lem1  27529  ostth2lem2  27545  ostth2lem3  27546  ostth3  27549  noextenddif  27580  noextendlt  27581  noextendgt  27582  nosupbnd1lem3  27622  nosupbnd1lem4  27623  nosupbnd1lem5  27624  nosupbnd1lem6  27625  noinfbnd1lem3  27637  noinfbnd1lem4  27638  noinfbnd1lem5  27639  noinfbnd1lem6  27640  noetasuplem4  27648  madecut  27794  cofcut2  27830  eucliddivs  28265  legov  28512  axsegcon  28854  axpaschlem  28867  0uhgrsubgr  29206  clwwlkf1  29978  upgr4cycl4dv4e  30114  eupth2lem3lem3  30159  nrt2irr  30402  nmblolbii  30728  nmbdoplbi  31953  nmcoplbi  31957  nmophmi  31960  nmbdfnlbi  31978  nmcfnlbi  31981  cnlnadjlem7  32002  nmopcoi  32024  resf1o  32653  muldivdid  32664  receqid  32668  xdivrec  32847  cycpmfvlem  33069  cycpmfv3  33072  lbsdiflsp0  33622  txomap  33824  unitdivcld  33891  measvunilem  34202  measvuni  34204  measssd  34205  measiuns  34207  measinblem  34210  measdivcst  34214  sibfof  34331  oddpwdc  34345  sseqfv1  34380  sseqfv2  34385  probun  34410  totprobd  34417  dstrvprob  34463  actfunsnrndisj  34596  reprsuc  34606  breprexplema  34621  subfaclim  35175  connpconn  35222  cvmliftlem2  35273  cvmliftlem6  35277  cvmliftlem7  35278  cvmliftlem8  35279  cvmliftlem9  35280  cvmliftlem10  35281  snmlff  35316  lineext  36064  hilbert1.1  36142  nn0prpwlem  36310  poimirlem1  37615  opnmbllem0  37650  ismblfin  37655  itgabsnc  37683  ftc1cnnclem  37685  bfplem1  37816  bfp  37818  lfl1  39063  lfladdcl  39064  eqlkr  39092  lkrlsp  39095  atcvrj2b  39426  3dim1  39461  3dim2  39462  llni2  39506  2llnjaN  39560  lvoli3  39571  lvoli2  39575  lncvrelatN  39775  lhpat4N  40038  lhpat3  40040  4atexlemex6  40068  ldilco  40110  ltrnid  40129  ltrnatb  40131  ltrnel  40133  ltrncnvel  40136  ltrncnv  40140  ltrn11at  40141  ltrneq  40143  trlat  40163  trlator0  40165  ltrnnidn  40168  trlid0  40170  trlnidatb  40171  trlnle  40180  trlval3  40181  trlval4  40182  cdlemc2  40186  cdlemc5  40189  cdlemc6  40190  cdlemc  40191  cdlemd2  40193  cdlemd9  40200  cdleme0e  40211  cdleme02N  40216  cdleme0ex1N  40217  cdleme3e  40226  cdleme3g  40228  cdleme3h  40229  cdleme3  40231  cdleme7aa  40236  cdleme7b  40238  cdleme7c  40239  cdleme7d  40240  cdleme7e  40241  cdleme7ga  40242  cdleme7  40243  cdleme9  40247  cdleme16aN  40253  cdleme11c  40255  cdleme11dN  40256  cdleme11e  40257  cdleme11h  40260  cdleme11j  40261  cdleme11k  40262  cdleme12  40265  cdleme21j  40330  cdleme26eALTN  40355  cdleme26f  40357  cdleme26f2  40359  cdlemefrs29bpre0  40390  cdleme35a  40442  cdleme35b  40444  cdleme35c  40445  cdleme35f  40448  cdleme36a  40454  cdleme38m  40457  cdlemeg46rgv  40522  cdlemeg46req  40523  cdlemf  40557  cdlemg2fvlem  40588  cdlemg2l  40597  cdlemg7N  40620  cdlemg12g  40643  cdlemg15  40650  cdlemg17h  40662  cdlemg17  40671  cdlemg19a  40677  cdlemg24  40682  cdlemg37  40683  cdlemg27a  40686  cdlemg31b0N  40688  cdlemg27b  40690  cdlemg31c  40693  cdlemg31d  40694  cdlemg35  40707  trljco  40734  tgrpgrplem  40743  cdlemh2  40810  tendoconid  40823  tendotr  40824  cdlemk35s-id  40932  cdlemk39s-id  40934  cdlemk53b  40950  cdlemk53  40951  cdlemk54  40952  cdleml3N  40972  cdleml5N  40974  tendospcanN  41017  diclss  41187  dihvalcq2  41241  dihord4  41252  dihord5b  41253  dihord5apre  41256  dihmeetlem1N  41284  dihmeetbclemN  41298  dihmeetlem20N  41320  dihmeetALTN  41321  dihatlat  41328  dihatexv  41332  dochkr1  41472  dochkr1OLDN  41473  lcfl7lem  41493  lclkrlem2m  41513  hdmaplna1  41901  hdmaplns1  41902  hdmaplnm1  41903  cxp111d  42330  eldioph2lem1  42748  fphpdo  42805  irrapxlem1  42810  irrapxlem2  42811  irrapxlem3  42812  irrapxlem5  42814  pellexlem2  42818  pell1234qrreccl  42842  pell1234qrmulcl  42843  pell1234qrdich  42849  pell1qr1  42859  pellqrexplicit  42865  pellfundex  42874  reglogltb  42879  reglogleb  42880  pellfund14  42886  rmxycomplete  42906  jm2.24nn  42948  jm2.17b  42950  jm2.17c  42951  jm2.18  42977  jm2.19lem2  42979  jm2.20nn  42986  jm2.16nn0  42993  jm3.1lem2  43007  areaquad  43205  clsk3nimkb  44029  lemuldiv3d  44159  lemuldiv4d  44160  stoweidlem1  45999  stoweidlem11  46009  stoweidlem14  46012  stoweidlem26  46024  stoweidlem34  46032  stoweidlem38  46036  stoweidlem60  46058  fourierdlem52  46156  etransclem38  46270  2tceilhalfelfzo1  47333  reuopreuprim  47527  quad1  47621  requad1  47623  requad2  47624  isubgr3stgrlem1  47965  isubgr3stgrlem3  47967  gpg3kgrtriexlem1  48074  gpg3kgrtriexlem5  48078  domnmsuppn0  48357  lincvalpr  48407  ldepspr  48462  islindeps2  48472  fldivexpfllog2  48554  eenglngeehlnmlem1  48726  eenglngeehlnmlem2  48727  rrx2linest  48731  prsthinc  49453