Theorem syl112anc 1401

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 520	. 2 ⊢ (𝜑 → (𝜃 ∧ 𝜏))
6		syl112anc.5	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ (𝜃 ∧ 𝜏)) → 𝜂)
7	1, 2, 5, 6	syl3anc 1398	1 ⊢ (𝜑 → 𝜂)

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  rmob2  3846  2nreu  4409  fveqf1o  7300  frrlem12  8290  enfixsn  9070  gruina  10798  grur1  10800  enqeq  10914  muldivdid  11904  recrec  11907  rec11r  11909  divdivdiv  11911  dmdcan  11920  ddcan  11924  rereccl  11928  div2neg  11933  divmuld  12008  divmul2d  12019  divmul3d  12020  divassd  12021  div12d  12022  div23d  12023  divdird  12024  divsubdird  12025  div11d  12026  ltmul12a  12066  ltdiv1  12074  ltrec  12092  lt2msq1  12094  lediv2  12100  supmul1  12179  qbtwnre  13220  xlemul1a  13309  xlemul1  13311  xadd4d  13324  quoremz  13884  quoremnn0ALT  13886  expgt1  14132  nnlesq  14237  expnbnd  14264  expmulnbnd  14267  discr1  14271  facubnd  14332  pfxsuffeqwrdeq  14731  01sqrexlem6  15294  mulcn2  15643  geomulcvg  15926  cvgrat  15933  eftlub  16160  eflegeo  16172  tanhlt1  16211  sin01bnd  16236  cos01bnd  16237  eirrlem  16255  bitsmod  16489  mulgcd  16601  mulgcddvds  16708  prmind2  16738  qnumgt0  16804  pcpremul  16898  fldivp1  16952  pcfaclem  16953  qexpz  16956  prmpwdvds  16959  pockthg  16961  prmreclem1  16971  prmreclem5  16975  4sqlem10  17002  4sqlem12  17011  4sqlem16  17015  4sqlem17  17016  vdwlem3  17038  vdwlem8  17043  vdwlem9  17044  0ram  17075  ramz2  17079  cat1lem  18148  odmulg  19621  dfod2  19629  odf1o1  19637  odf1o2  19638  sylow3lem4  19695  ablsub4  19875  odadd1  19913  odadd2  19914  ablfacrp2  20134  ablfac1b  20137  ablfac1eu  20140  pgpfac1lem3a  20143  pgpfaclem2  20149  ablsimpgfindlem1  20174  chrcong  21677  znrrg  21715  cygznlem1  21716  chpdmatlem3  22997  txdis  23789  txdis1cn  23792  ptunhmeo  23965  qustgplem  24278  blcld  24662  nlmvscnlem2  24842  blcvx  24955  metds0  25008  metdseq0  25012  icopnfcnv  25101  lebnumii  25125  ipcau2  25393  tcphcphlem1  25394  ipcnlem2  25403  csbren  25558  trirn  25559  dyadf  25750  dyadovol  25752  dyaddisjlem  25754  dyadmaxlem  25756  opnmbllem  25760  mbfmulc2lem  25806  mbfi1fseqlem4  25877  mbfi1fseqlem5  25878  mbfi1fseqlem6  25879  itg2mulclem  25905  itg2monolem1  25909  itg2monolem3  25911  itg2cnlem2  25921  itgabs  25994  dvlip  26152  dvlt0  26164  dvcvx  26179  ftc1lem4  26198  dgrcolem2  26431  aaliou3lem2  26506  aaliou3lem9  26513  itgulm  26571  radcnvlem1  26576  abelthlem2  26595  abelthlem7  26601  tangtx  26670  cosne0  26694  cosordlem  26695  tanord1  26702  logdivlti  26785  logcnlem4  26810  logf1o2  26815  cxpcn3lem  26912  cxpaddle  26917  ang180lem2  26975  atanlogsublem  27080  atantan  27088  atanbndlem  27090  atans2  27096  leibpi  27107  log2tlbnd  27110  birthdaylem3  27118  efrlim  27134  jensenlem2  27152  zetacvg  27179  ftalem1  27237  ftalem5  27241  basellem1  27245  basellem4  27248  fsumdvdsdiaglem  27347  dvdsflf1o  27351  fsumfldivdiaglem  27353  ppiub  27368  mersenne  27391  dchrptlem1  27428  bposlem1  27448  bposlem2  27449  bposlem4  27451  lgsdilem  27488  lgseisenlem1  27539  lgseisenlem2  27540  lgseisenlem3  27541  lgsquadlem1  27544  lgsquadlem2  27545  2sqlem3  27584  2sqlem8  27590  2sqlem11  27593  2sqblem  27595  chebbnd1lem2  27634  chebbnd1lem3  27635  rplogsumlem1  27648  rplogsumlem2  27649  dchrisumlem1  27653  dchrmusum2  27658  dchrisum0flblem1  27672  mulog2sumlem1  27698  logdivbnd  27720  pntpbnd1a  27749  pntpbnd1  27750  pntpbnd2  27751  pntlemh  27763  pntlemr  27766  pntlemk  27770  pntlemo  27771  ostth2lem1  27782  ostth2lem2  27798  ostth2lem3  27799  ostth3  27802  noextenddif  27832  noextendlt  27833  noextendgt  27834  nosupbnd1lem3  27874  nosupbnd1lem4  27875  nosupbnd1lem5  27876  nosupbnd1lem6  27877  noinfbnd1lem3  27889  noinfbnd1lem4  27890  noinfbnd1lem5  27891  noinfbnd1lem6  27892  noetasuplem4  27900  madecut  28076  cofcut2  28115  eucliddivs  28569  legov  28854  axsegcon  29277  axpaschlem  29290  0uhgrsubgr  29629  clwwlkf1  30400  upgr4cycl4dv4e  30536  eupth2lem3lem3  30581  nrt2irr  30824  nmblolbii  31151  nmbdoplbi  32376  nmcoplbi  32380  nmophmi  32383  nmbdfnlbi  32401  nmcfnlbi  32404  cnlnadjlem7  32425  nmopcoi  32447  resf1o  33075  receqid  33089  xdivrec  33246  cycpmfvlem  33432  cycpmfv3  33435  lbsdiflsp0  34016  txomap  34224  unitdivcld  34291  measvunilem  34602  measvuni  34604  measssd  34605  measiuns  34607  measinblem  34610  measdivcst  34614  sibfof  34730  oddpwdc  34744  sseqfv1  34779  sseqfv2  34784  probun  34809  totprobd  34816  dstrvprob  34862  actfunsnrndisj  34992  reprsuc  35002  breprexplema  35017  subfaclim  35680  connpconn  35727  cvmliftlem2  35778  cvmliftlem6  35782  cvmliftlem7  35783  cvmliftlem8  35784  cvmliftlem9  35785  cvmliftlem10  35786  snmlff  35821  lineext  36568  hilbert1.1  36646  nn0prpwlem  36833  poimirlem1  38272  opnmbllem0  38307  ismblfin  38312  itgabsnc  38340  ftc1cnnclem  38342  bfplem1  38473  bfp  38475  lfl1  39844  lfladdcl  39845  eqlkr  39873  lkrlsp  39876  atcvrj2b  40206  3dim1  40241  3dim2  40242  llni2  40286  2llnjaN  40340  lvoli3  40351  lvoli2  40355  lncvrelatN  40555  lhpat4N  40818  lhpat3  40820  4atexlemex6  40848  ldilco  40890  ltrnid  40909  ltrnatb  40911  ltrnel  40913  ltrncnvel  40916  ltrncnv  40920  ltrn11at  40921  ltrneq  40923  trlat  40943  trlator0  40945  ltrnnidn  40948  trlid0  40950  trlnidatb  40951  trlnle  40960  trlval3  40961  trlval4  40962  cdlemc2  40966  cdlemc5  40969  cdlemc6  40970  cdlemc  40971  cdlemd2  40973  cdlemd9  40980  cdleme0e  40991  cdleme02N  40996  cdleme0ex1N  40997  cdleme3e  41006  cdleme3g  41008  cdleme3h  41009  cdleme3  41011  cdleme7aa  41016  cdleme7b  41018  cdleme7c  41019  cdleme7d  41020  cdleme7e  41021  cdleme7ga  41022  cdleme7  41023  cdleme9  41027  cdleme16aN  41033  cdleme11c  41035  cdleme11dN  41036  cdleme11e  41037  cdleme11h  41040  cdleme11j  41041  cdleme11k  41042  cdleme12  41045  cdleme21j  41110  cdleme26eALTN  41135  cdleme26f  41137  cdleme26f2  41139  cdlemefrs29bpre0  41170  cdleme35a  41222  cdleme35b  41224  cdleme35c  41225  cdleme35f  41228  cdleme36a  41234  cdleme38m  41237  cdlemeg46rgv  41302  cdlemeg46req  41303  cdlemf  41337  cdlemg2fvlem  41368  cdlemg2l  41377  cdlemg7N  41400  cdlemg12g  41423  cdlemg15  41430  cdlemg17h  41442  cdlemg17  41451  cdlemg19a  41457  cdlemg24  41462  cdlemg37  41463  cdlemg27a  41466  cdlemg31b0N  41468  cdlemg27b  41470  cdlemg31c  41473  cdlemg31d  41474  cdlemg35  41487  trljco  41514  tgrpgrplem  41523  cdlemh2  41590  tendoconid  41603  tendotr  41604  cdlemk35s-id  41712  cdlemk39s-id  41714  cdlemk53b  41730  cdlemk53  41731  cdlemk54  41732  cdleml3N  41752  cdleml5N  41754  tendospcanN  41797  diclss  41967  dihvalcq2  42021  dihord4  42032  dihord5b  42033  dihord5apre  42036  dihmeetlem1N  42064  dihmeetbclemN  42078  dihmeetlem20N  42100  dihmeetALTN  42101  dihatlat  42108  dihatexv  42112  dochkr1  42252  dochkr1OLDN  42253  lcfl7lem  42273  lclkrlem2m  42293  hdmaplna1  42681  hdmaplns1  42682  hdmaplnm1  42683  cxp111d  43103  eldioph2lem1  43491  fphpdo  43544  irrapxlem1  43549  irrapxlem2  43550  irrapxlem3  43551  irrapxlem5  43553  pellexlem2  43557  pell1234qrreccl  43581  pell1234qrmulcl  43582  pell1234qrdich  43588  pell1qr1  43598  pellqrexplicit  43604  pellfundex  43613  reglogltb  43618  reglogleb  43619  pellfund14  43625  rmxycomplete  43644  jm2.24nn  43686  jm2.17b  43688  jm2.17c  43689  jm2.18  43715  jm2.19lem2  43717  jm2.20nn  43724  jm2.16nn0  43731  jm3.1lem2  43745  areaquad  43943  clsk3nimkb  44766  lemuldiv3d  44896  lemuldiv4d  44897  stoweidlem1  46715  stoweidlem11  46725  stoweidlem14  46728  stoweidlem26  46740  stoweidlem34  46748  stoweidlem38  46752  stoweidlem60  46774  fourierdlem52  46872  etransclem38  46986  2tceilhalfelfzo1  48073  reuopreuprim  48275  nprmdvdsfacm1lem4  48375  quad1  48385  requad1  48387  requad2  48388  isubgr3stgrlem1  48731  isubgr3stgrlem3  48733  gpg3kgrtriexlem1  48848  gpg3kgrtriexlem5  48852  domnmsuppn0  49149  lincvalpr  49198  ldepspr  49253  islindeps2  49263  fldivexpfllog2  49345  eenglngeehlnmlem1  49517  eenglngeehlnmlem2  49518  rrx2linest  49522  prsthinc  50242