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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1089

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 400  df-3an 1091

This theorem is referenced by:  rmob2  3804  2nreu  4356  fveqf1o  7113  frrlem12  8038  enfixsn  8754  gruina  10432  grur1  10434  enqeq  10548  recrec  11529  rec11r  11531  divdivdiv  11533  dmdcan  11542  ddcan  11546  rereccl  11550  div2neg  11555  divmuld  11630  divmul2d  11641  divmul3d  11642  divassd  11643  div12d  11644  div23d  11645  divdird  11646  divsubdird  11647  div11d  11648  ltmul12a  11688  ltdiv1  11696  ltrec  11714  lt2msq1  11716  lediv2  11722  supmul1  11801  qbtwnre  12789  xlemul1a  12878  xlemul1  12880  xadd4d  12893  quoremz  13428  quoremnn0ALT  13430  expgt1  13673  nnlesq  13774  expnbnd  13799  expmulnbnd  13802  discr1  13806  facubnd  13866  pfxsuffeqwrdeq  14263  sqrlem6  14811  mulcn2  15157  geomulcvg  15440  cvgrat  15447  eftlub  15670  eflegeo  15682  tanhlt1  15721  sin01bnd  15746  cos01bnd  15747  eirrlem  15765  bitsmod  15995  mulgcd  16108  mulgcddvds  16212  prmind2  16242  qnumgt0  16306  pcpremul  16396  fldivp1  16450  pcfaclem  16451  qexpz  16454  prmpwdvds  16457  pockthg  16459  prmreclem1  16469  prmreclem5  16473  4sqlem10  16500  4sqlem12  16509  4sqlem16  16513  4sqlem17  16514  vdwlem3  16536  vdwlem8  16541  vdwlem9  16542  0ram  16573  ramz2  16577  cat1lem  17602  odmulg  18947  dfod2  18955  odf1o1  18961  odf1o2  18962  sylow3lem4  19019  ablsub4  19198  odadd1  19233  odadd2  19234  ablfacrp2  19454  ablfac1b  19457  ablfac1eu  19460  pgpfac1lem3a  19463  pgpfaclem2  19469  ablsimpgfindlem1  19494  chrcong  20494  znrrg  20530  cygznlem1  20531  chpdmatlem3  21737  txdis  22529  txdis1cn  22532  ptunhmeo  22705  qustgplem  23018  blcld  23403  nlmvscnlem2  23583  blcvx  23695  metds0  23747  metdseq0  23751  icopnfcnv  23839  lebnumii  23863  ipcau2  24131  tcphcphlem1  24132  ipcnlem2  24141  csbren  24296  trirn  24297  dyadf  24488  dyadovol  24490  dyaddisjlem  24492  dyadmaxlem  24494  opnmbllem  24498  mbfmulc2lem  24544  mbfi1fseqlem4  24616  mbfi1fseqlem5  24617  mbfi1fseqlem6  24618  itg2mulclem  24644  itg2monolem1  24648  itg2monolem3  24650  itg2cnlem2  24660  itgabs  24732  dvlip  24890  dvlt0  24902  dvcvx  24917  ftc1lem4  24936  dgrcolem2  25168  aaliou3lem2  25236  aaliou3lem9  25243  itgulm  25300  radcnvlem1  25305  abelthlem2  25324  abelthlem7  25330  tangtx  25395  cosne0  25418  cosordlem  25419  tanord1  25426  logdivlti  25508  logcnlem4  25533  logf1o2  25538  cxpcn3lem  25633  cxpaddle  25638  ang180lem2  25693  atanlogsublem  25798  atantan  25806  atanbndlem  25808  atans2  25814  leibpi  25825  log2tlbnd  25828  birthdaylem3  25836  efrlim  25852  jensenlem2  25870  zetacvg  25897  ftalem1  25955  ftalem5  25959  basellem1  25963  basellem4  25966  fsumdvdsdiaglem  26065  dvdsflf1o  26069  fsumfldivdiaglem  26071  ppiub  26085  mersenne  26108  dchrptlem1  26145  bposlem1  26165  bposlem2  26166  bposlem4  26168  lgsdilem  26205  lgseisenlem1  26256  lgseisenlem2  26257  lgseisenlem3  26258  lgsquadlem1  26261  lgsquadlem2  26262  2sqlem3  26301  2sqlem8  26307  2sqlem11  26310  2sqblem  26312  chebbnd1lem2  26351  chebbnd1lem3  26352  rplogsumlem1  26365  rplogsumlem2  26366  dchrisumlem1  26370  dchrmusum2  26375  dchrisum0flblem1  26389  mulog2sumlem1  26415  logdivbnd  26437  pntpbnd1a  26466  pntpbnd1  26467  pntpbnd2  26468  pntlemh  26480  pntlemr  26483  pntlemk  26487  pntlemo  26488  ostth2lem1  26499  ostth2lem2  26515  ostth2lem3  26516  ostth3  26519  legov  26676  axsegcon  27018  axpaschlem  27031  0uhgrsubgr  27367  clwwlkf1  28132  upgr4cycl4dv4e  28268  eupth2lem3lem3  28313  nmblolbii  28880  nmbdoplbi  30105  nmcoplbi  30109  nmophmi  30112  nmbdfnlbi  30130  nmcfnlbi  30133  cnlnadjlem7  30154  nmopcoi  30176  resf1o  30785  xdivrec  30921  cycpmfvlem  31098  cycpmfv3  31101  lbsdiflsp0  31421  txomap  31498  unitdivcld  31565  measvunilem  31892  measvuni  31894  measssd  31895  measiuns  31897  measinblem  31900  measdivcst  31904  sibfof  32019  oddpwdc  32033  sseqfv1  32068  sseqfv2  32073  probun  32098  totprobd  32105  dstrvprob  32150  actfunsnrndisj  32297  reprsuc  32307  breprexplema  32322  subfaclim  32863  connpconn  32910  cvmliftlem2  32961  cvmliftlem6  32965  cvmliftlem7  32966  cvmliftlem8  32967  cvmliftlem9  32968  cvmliftlem10  32969  snmlff  33004  noextenddif  33608  noextendlt  33609  noextendgt  33610  nosupbnd1lem3  33650  nosupbnd1lem4  33651  nosupbnd1lem5  33652  nosupbnd1lem6  33653  noinfbnd1lem3  33665  noinfbnd1lem4  33666  noinfbnd1lem5  33667  noinfbnd1lem6  33668  noetasuplem4  33676  madecut  33802  cofcut2  33828  lineext  34115  hilbert1.1  34193  nn0prpwlem  34248  poimirlem1  35515  opnmbllem0  35550  ismblfin  35555  itgabsnc  35583  ftc1cnnclem  35585  bfplem1  35717  bfp  35719  lfl1  36821  lfladdcl  36822  eqlkr  36850  lkrlsp  36853  atcvrj2b  37183  3dim1  37218  3dim2  37219  llni2  37263  2llnjaN  37317  lvoli3  37328  lvoli2  37332  lncvrelatN  37532  lhpat4N  37795  lhpat3  37797  4atexlemex6  37825  ldilco  37867  ltrnid  37886  ltrnatb  37888  ltrnel  37890  ltrncnvel  37893  ltrncnv  37897  ltrn11at  37898  ltrneq  37900  trlat  37920  trlator0  37922  ltrnnidn  37925  trlid0  37927  trlnidatb  37928  trlnle  37937  trlval3  37938  trlval4  37939  cdlemc2  37943  cdlemc5  37946  cdlemc6  37947  cdlemc  37948  cdlemd2  37950  cdlemd9  37957  cdleme0e  37968  cdleme02N  37973  cdleme0ex1N  37974  cdleme3e  37983  cdleme3g  37985  cdleme3h  37986  cdleme3  37988  cdleme7aa  37993  cdleme7b  37995  cdleme7c  37996  cdleme7d  37997  cdleme7e  37998  cdleme7ga  37999  cdleme7  38000  cdleme9  38004  cdleme16aN  38010  cdleme11c  38012  cdleme11dN  38013  cdleme11e  38014  cdleme11h  38017  cdleme11j  38018  cdleme11k  38019  cdleme12  38022  cdleme21j  38087  cdleme26eALTN  38112  cdleme26f  38114  cdleme26f2  38116  cdlemefrs29bpre0  38147  cdleme35a  38199  cdleme35b  38201  cdleme35c  38202  cdleme35f  38205  cdleme36a  38211  cdleme38m  38214  cdlemeg46rgv  38279  cdlemeg46req  38280  cdlemf  38314  cdlemg2fvlem  38345  cdlemg2l  38354  cdlemg7N  38377  cdlemg12g  38400  cdlemg15  38407  cdlemg17h  38419  cdlemg17  38428  cdlemg19a  38434  cdlemg24  38439  cdlemg37  38440  cdlemg27a  38443  cdlemg31b0N  38445  cdlemg27b  38447  cdlemg31c  38450  cdlemg31d  38451  cdlemg35  38464  trljco  38491  tgrpgrplem  38500  cdlemh2  38567  tendoconid  38580  tendotr  38581  cdlemk35s-id  38689  cdlemk39s-id  38691  cdlemk53b  38707  cdlemk53  38708  cdlemk54  38709  cdleml3N  38729  cdleml5N  38731  tendospcanN  38774  diclss  38944  dihvalcq2  38998  dihord4  39009  dihord5b  39010  dihord5apre  39013  dihmeetlem1N  39041  dihmeetbclemN  39055  dihmeetlem20N  39077  dihmeetALTN  39078  dihatlat  39085  dihatexv  39089  dochkr1  39229  dochkr1OLDN  39230  lcfl7lem  39250  lclkrlem2m  39270  hdmaplna1  39658  hdmaplns1  39659  hdmaplnm1  39660  eldioph2lem1  40285  fphpdo  40342  irrapxlem1  40347  irrapxlem2  40348  irrapxlem3  40349  irrapxlem5  40351  pellexlem2  40355  pell1234qrreccl  40379  pell1234qrmulcl  40380  pell1234qrdich  40386  pell1qr1  40396  pellqrexplicit  40402  pellfundex  40411  reglogltb  40416  reglogleb  40417  pellfund14  40423  rmxycomplete  40442  jm2.24nn  40484  jm2.17b  40486  jm2.17c  40487  jm2.18  40513  jm2.19lem2  40515  jm2.20nn  40522  jm2.16nn0  40529  jm3.1lem2  40543  areaquad  40750  clsk3nimkb  41327  lemuldiv3d  41458  lemuldiv4d  41459  stoweidlem1  43217  stoweidlem11  43227  stoweidlem14  43230  stoweidlem26  43242  stoweidlem34  43250  stoweidlem38  43254  stoweidlem60  43276  fourierdlem52  43374  etransclem38  43488  reuopreuprim  44651  quad1  44745  requad1  44747  requad2  44748  domnmsuppn0  45378  lincvalpr  45432  ldepspr  45487  islindeps2  45497  fldivexpfllog2  45584  eenglngeehlnmlem1  45756  eenglngeehlnmlem2  45757  rrx2linest  45761  prsthinc  46008