Theorem syl112anc 1374

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

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1087

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 206  df-an 398  df-3an 1089

This theorem is referenced by:  rmob2  3830  2nreu  4381  fveqf1o  7207  frrlem12  8144  enfixsn  8906  gruina  10620  grur1  10622  enqeq  10736  recrec  11718  rec11r  11720  divdivdiv  11722  dmdcan  11731  ddcan  11735  rereccl  11739  div2neg  11744  divmuld  11819  divmul2d  11830  divmul3d  11831  divassd  11832  div12d  11833  div23d  11834  divdird  11835  divsubdird  11836  div11d  11837  ltmul12a  11877  ltdiv1  11885  ltrec  11903  lt2msq1  11905  lediv2  11911  supmul1  11990  qbtwnre  12979  xlemul1a  13068  xlemul1  13070  xadd4d  13083  quoremz  13621  quoremnn0ALT  13623  expgt1  13867  nnlesq  13968  expnbnd  13993  expmulnbnd  13996  discr1  14000  facubnd  14060  pfxsuffeqwrdeq  14456  sqrlem6  15004  mulcn2  15350  geomulcvg  15633  cvgrat  15640  eftlub  15863  eflegeo  15875  tanhlt1  15914  sin01bnd  15939  cos01bnd  15940  eirrlem  15958  bitsmod  16188  mulgcd  16301  mulgcddvds  16405  prmind2  16435  qnumgt0  16499  pcpremul  16589  fldivp1  16643  pcfaclem  16644  qexpz  16647  prmpwdvds  16650  pockthg  16652  prmreclem1  16662  prmreclem5  16666  4sqlem10  16693  4sqlem12  16702  4sqlem16  16706  4sqlem17  16707  vdwlem3  16729  vdwlem8  16734  vdwlem9  16735  0ram  16766  ramz2  16770  cat1lem  17856  odmulg  19208  dfod2  19216  odf1o1  19222  odf1o2  19223  sylow3lem4  19280  ablsub4  19459  odadd1  19494  odadd2  19495  ablfacrp2  19715  ablfac1b  19718  ablfac1eu  19721  pgpfac1lem3a  19724  pgpfaclem2  19730  ablsimpgfindlem1  19755  chrcong  20778  znrrg  20818  cygznlem1  20819  chpdmatlem3  22034  txdis  22828  txdis1cn  22831  ptunhmeo  23004  qustgplem  23317  blcld  23706  nlmvscnlem2  23894  blcvx  24006  metds0  24058  metdseq0  24062  icopnfcnv  24150  lebnumii  24174  ipcau2  24443  tcphcphlem1  24444  ipcnlem2  24453  csbren  24608  trirn  24609  dyadf  24800  dyadovol  24802  dyaddisjlem  24804  dyadmaxlem  24806  opnmbllem  24810  mbfmulc2lem  24856  mbfi1fseqlem4  24928  mbfi1fseqlem5  24929  mbfi1fseqlem6  24930  itg2mulclem  24956  itg2monolem1  24960  itg2monolem3  24962  itg2cnlem2  24972  itgabs  25044  dvlip  25202  dvlt0  25214  dvcvx  25229  ftc1lem4  25248  dgrcolem2  25480  aaliou3lem2  25548  aaliou3lem9  25555  itgulm  25612  radcnvlem1  25617  abelthlem2  25636  abelthlem7  25642  tangtx  25707  cosne0  25730  cosordlem  25731  tanord1  25738  logdivlti  25820  logcnlem4  25845  logf1o2  25850  cxpcn3lem  25945  cxpaddle  25950  ang180lem2  26005  atanlogsublem  26110  atantan  26118  atanbndlem  26120  atans2  26126  leibpi  26137  log2tlbnd  26140  birthdaylem3  26148  efrlim  26164  jensenlem2  26182  zetacvg  26209  ftalem1  26267  ftalem5  26271  basellem1  26275  basellem4  26278  fsumdvdsdiaglem  26377  dvdsflf1o  26381  fsumfldivdiaglem  26383  ppiub  26397  mersenne  26420  dchrptlem1  26457  bposlem1  26477  bposlem2  26478  bposlem4  26480  lgsdilem  26517  lgseisenlem1  26568  lgseisenlem2  26569  lgseisenlem3  26570  lgsquadlem1  26573  lgsquadlem2  26574  2sqlem3  26613  2sqlem8  26619  2sqlem11  26622  2sqblem  26624  chebbnd1lem2  26663  chebbnd1lem3  26664  rplogsumlem1  26677  rplogsumlem2  26678  dchrisumlem1  26682  dchrmusum2  26687  dchrisum0flblem1  26701  mulog2sumlem1  26727  logdivbnd  26749  pntpbnd1a  26778  pntpbnd1  26779  pntpbnd2  26780  pntlemh  26792  pntlemr  26795  pntlemk  26799  pntlemo  26800  ostth2lem1  26811  ostth2lem2  26827  ostth2lem3  26828  ostth3  26831  legov  26991  axsegcon  27340  axpaschlem  27353  0uhgrsubgr  27691  clwwlkf1  28458  upgr4cycl4dv4e  28594  eupth2lem3lem3  28639  nmblolbii  29206  nmbdoplbi  30431  nmcoplbi  30435  nmophmi  30438  nmbdfnlbi  30456  nmcfnlbi  30459  cnlnadjlem7  30480  nmopcoi  30502  resf1o  31110  xdivrec  31246  cycpmfvlem  31424  cycpmfv3  31427  lbsdiflsp0  31752  txomap  31829  unitdivcld  31896  measvunilem  32225  measvuni  32227  measssd  32228  measiuns  32230  measinblem  32233  measdivcst  32237  sibfof  32352  oddpwdc  32366  sseqfv1  32401  sseqfv2  32406  probun  32431  totprobd  32438  dstrvprob  32483  actfunsnrndisj  32630  reprsuc  32640  breprexplema  32655  subfaclim  33195  connpconn  33242  cvmliftlem2  33293  cvmliftlem6  33297  cvmliftlem7  33298  cvmliftlem8  33299  cvmliftlem9  33300  cvmliftlem10  33301  snmlff  33336  noextenddif  33916  noextendlt  33917  noextendgt  33918  nosupbnd1lem3  33958  nosupbnd1lem4  33959  nosupbnd1lem5  33960  nosupbnd1lem6  33961  noinfbnd1lem3  33973  noinfbnd1lem4  33974  noinfbnd1lem5  33975  noinfbnd1lem6  33976  noetasuplem4  33984  madecut  34110  cofcut2  34136  lineext  34423  hilbert1.1  34501  nn0prpwlem  34556  poimirlem1  35822  opnmbllem0  35857  ismblfin  35862  itgabsnc  35890  ftc1cnnclem  35892  bfplem1  36024  bfp  36026  lfl1  37126  lfladdcl  37127  eqlkr  37155  lkrlsp  37158  atcvrj2b  37488  3dim1  37523  3dim2  37524  llni2  37568  2llnjaN  37622  lvoli3  37633  lvoli2  37637  lncvrelatN  37837  lhpat4N  38100  lhpat3  38102  4atexlemex6  38130  ldilco  38172  ltrnid  38191  ltrnatb  38193  ltrnel  38195  ltrncnvel  38198  ltrncnv  38202  ltrn11at  38203  ltrneq  38205  trlat  38225  trlator0  38227  ltrnnidn  38230  trlid0  38232  trlnidatb  38233  trlnle  38242  trlval3  38243  trlval4  38244  cdlemc2  38248  cdlemc5  38251  cdlemc6  38252  cdlemc  38253  cdlemd2  38255  cdlemd9  38262  cdleme0e  38273  cdleme02N  38278  cdleme0ex1N  38279  cdleme3e  38288  cdleme3g  38290  cdleme3h  38291  cdleme3  38293  cdleme7aa  38298  cdleme7b  38300  cdleme7c  38301  cdleme7d  38302  cdleme7e  38303  cdleme7ga  38304  cdleme7  38305  cdleme9  38309  cdleme16aN  38315  cdleme11c  38317  cdleme11dN  38318  cdleme11e  38319  cdleme11h  38322  cdleme11j  38323  cdleme11k  38324  cdleme12  38327  cdleme21j  38392  cdleme26eALTN  38417  cdleme26f  38419  cdleme26f2  38421  cdlemefrs29bpre0  38452  cdleme35a  38504  cdleme35b  38506  cdleme35c  38507  cdleme35f  38510  cdleme36a  38516  cdleme38m  38519  cdlemeg46rgv  38584  cdlemeg46req  38585  cdlemf  38619  cdlemg2fvlem  38650  cdlemg2l  38659  cdlemg7N  38682  cdlemg12g  38705  cdlemg15  38712  cdlemg17h  38724  cdlemg17  38733  cdlemg19a  38739  cdlemg24  38744  cdlemg37  38745  cdlemg27a  38748  cdlemg31b0N  38750  cdlemg27b  38752  cdlemg31c  38755  cdlemg31d  38756  cdlemg35  38769  trljco  38796  tgrpgrplem  38805  cdlemh2  38872  tendoconid  38885  tendotr  38886  cdlemk35s-id  38994  cdlemk39s-id  38996  cdlemk53b  39012  cdlemk53  39013  cdlemk54  39014  cdleml3N  39034  cdleml5N  39036  tendospcanN  39079  diclss  39249  dihvalcq2  39303  dihord4  39314  dihord5b  39315  dihord5apre  39318  dihmeetlem1N  39346  dihmeetbclemN  39360  dihmeetlem20N  39382  dihmeetALTN  39383  dihatlat  39390  dihatexv  39394  dochkr1  39534  dochkr1OLDN  39535  lcfl7lem  39555  lclkrlem2m  39575  hdmaplna1  39963  hdmaplns1  39964  hdmaplnm1  39965  eldioph2lem1  40619  fphpdo  40676  irrapxlem1  40681  irrapxlem2  40682  irrapxlem3  40683  irrapxlem5  40685  pellexlem2  40689  pell1234qrreccl  40713  pell1234qrmulcl  40714  pell1234qrdich  40720  pell1qr1  40730  pellqrexplicit  40736  pellfundex  40745  reglogltb  40750  reglogleb  40751  pellfund14  40757  rmxycomplete  40777  jm2.24nn  40819  jm2.17b  40821  jm2.17c  40822  jm2.18  40848  jm2.19lem2  40850  jm2.20nn  40857  jm2.16nn0  40864  jm3.1lem2  40878  areaquad  41085  clsk3nimkb  41688  lemuldiv3d  41819  lemuldiv4d  41820  stoweidlem1  43591  stoweidlem11  43601  stoweidlem14  43604  stoweidlem26  43616  stoweidlem34  43624  stoweidlem38  43628  stoweidlem60  43650  fourierdlem52  43748  etransclem38  43862  reuopreuprim  45036  quad1  45130  requad1  45132  requad2  45133  domnmsuppn0  45763  lincvalpr  45817  ldepspr  45872  islindeps2  45882  fldivexpfllog2  45969  eenglngeehlnmlem1  46141  eenglngeehlnmlem2  46142  rrx2linest  46146  prsthinc  46393