Theorem syl112anc 1370

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  rmob2  3876  2nreu  4393  fveqf1o  7058  enfixsn  8626  gruina  10240  grur1  10242  enqeq  10356  recrec  11337  rec11r  11339  divdivdiv  11341  dmdcan  11350  ddcan  11354  rereccl  11358  div2neg  11363  divmuld  11438  divmul2d  11449  divmul3d  11450  divassd  11451  div12d  11452  div23d  11453  divdird  11454  divsubdird  11455  div11d  11456  ltmul12a  11496  ltdiv1  11504  ltrec  11522  lt2msq1  11524  lediv2  11530  supmul1  11610  qbtwnre  12593  xlemul1a  12682  xlemul1  12684  xadd4d  12697  quoremz  13224  quoremnn0ALT  13226  expgt1  13468  nnlesq  13569  expnbnd  13594  expmulnbnd  13597  discr1  13601  facubnd  13661  hashf1lem1  13814  pfxsuffeqwrdeq  14060  sqrlem6  14607  mulcn2  14952  geomulcvg  15232  cvgrat  15239  eftlub  15462  eflegeo  15474  tanhlt1  15513  sin01bnd  15538  cos01bnd  15539  eirrlem  15557  bitsmod  15785  mulgcd  15896  mulgcddvds  15999  prmind2  16029  qnumgt0  16090  pcpremul  16180  fldivp1  16233  pcfaclem  16234  qexpz  16237  prmpwdvds  16240  pockthg  16242  prmreclem1  16252  prmreclem5  16256  4sqlem10  16283  4sqlem12  16292  4sqlem16  16296  4sqlem17  16297  vdwlem3  16319  vdwlem8  16324  vdwlem9  16325  0ram  16356  ramz2  16360  odmulg  18683  dfod2  18691  odf1o1  18697  odf1o2  18698  sylow3lem4  18755  ablsub4  18933  odadd1  18968  odadd2  18969  ablfacrp2  19189  ablfac1b  19192  ablfac1eu  19195  pgpfac1lem3a  19198  pgpfaclem2  19204  ablsimpgfindlem1  19229  chrcong  20676  znrrg  20712  cygznlem1  20713  chpdmatlem3  21448  txdis  22240  txdis1cn  22243  ptunhmeo  22416  qustgplem  22729  blcld  23115  nlmvscnlem2  23294  blcvx  23406  metds0  23458  metdseq0  23462  icopnfcnv  23546  lebnumii  23570  ipcau2  23837  tcphcphlem1  23838  ipcnlem2  23847  csbren  24002  trirn  24003  dyadf  24192  dyadovol  24194  dyaddisjlem  24196  dyadmaxlem  24198  opnmbllem  24202  mbfmulc2lem  24248  mbfi1fseqlem4  24319  mbfi1fseqlem5  24320  mbfi1fseqlem6  24321  itg2mulclem  24347  itg2monolem1  24351  itg2monolem3  24353  itg2cnlem2  24363  itgabs  24435  dvlip  24590  dvlt0  24602  dvcvx  24617  ftc1lem4  24636  dgrcolem2  24864  aaliou3lem2  24932  aaliou3lem9  24939  itgulm  24996  radcnvlem1  25001  abelthlem2  25020  abelthlem7  25026  tangtx  25091  cosne0  25114  cosordlem  25115  tanord1  25121  logdivlti  25203  logcnlem4  25228  logf1o2  25233  cxpcn3lem  25328  cxpaddle  25333  ang180lem2  25388  atanlogsublem  25493  atantan  25501  atanbndlem  25503  atans2  25509  leibpi  25520  log2tlbnd  25523  birthdaylem3  25531  efrlim  25547  jensenlem2  25565  zetacvg  25592  ftalem1  25650  ftalem5  25654  basellem1  25658  basellem4  25661  fsumdvdsdiaglem  25760  dvdsflf1o  25764  fsumfldivdiaglem  25766  ppiub  25780  mersenne  25803  dchrptlem1  25840  bposlem1  25860  bposlem2  25861  bposlem4  25863  lgsdilem  25900  lgseisenlem1  25951  lgseisenlem2  25952  lgseisenlem3  25953  lgsquadlem1  25956  lgsquadlem2  25957  2sqlem3  25996  2sqlem8  26002  2sqlem11  26005  2sqblem  26007  chebbnd1lem2  26046  chebbnd1lem3  26047  rplogsumlem1  26060  rplogsumlem2  26061  dchrisumlem1  26065  dchrmusum2  26070  dchrisum0flblem1  26084  mulog2sumlem1  26110  logdivbnd  26132  pntpbnd1a  26161  pntpbnd1  26162  pntpbnd2  26163  pntlemh  26175  pntlemr  26178  pntlemk  26182  pntlemo  26183  ostth2lem1  26194  ostth2lem2  26210  ostth2lem3  26211  ostth3  26214  legov  26371  axsegcon  26713  axpaschlem  26726  0uhgrsubgr  27061  clwwlkf1  27828  upgr4cycl4dv4e  27964  eupth2lem3lem3  28009  nmblolbii  28576  nmbdoplbi  29801  nmcoplbi  29805  nmophmi  29808  nmbdfnlbi  29826  nmcfnlbi  29829  cnlnadjlem7  29850  nmopcoi  29872  resf1o  30466  xdivrec  30603  cycpmfvlem  30754  cycpmfv3  30757  lbsdiflsp0  31022  txomap  31098  unitdivcld  31144  measvunilem  31471  measvuni  31473  measssd  31474  measiuns  31476  measinblem  31479  measdivcst  31483  sibfof  31598  oddpwdc  31612  sseqfv1  31647  sseqfv2  31652  probun  31677  totprobd  31684  dstrvprob  31729  actfunsnrndisj  31876  reprsuc  31886  breprexplema  31901  subfaclim  32435  connpconn  32482  cvmliftlem2  32533  cvmliftlem6  32537  cvmliftlem7  32538  cvmliftlem8  32539  cvmliftlem9  32540  cvmliftlem10  32541  snmlff  32576  frrlem12  33134  noextenddif  33175  noextendlt  33176  noextendgt  33177  nosupbnd1lem3  33210  nosupbnd1lem4  33211  nosupbnd1lem5  33212  nosupbnd1lem6  33213  noetalem3  33219  lineext  33537  hilbert1.1  33615  nn0prpwlem  33670  poimirlem1  34908  opnmbllem0  34943  ismblfin  34948  itgabsnc  34976  ftc1cnnclem  34980  bfplem1  35115  bfp  35117  lfl1  36221  lfladdcl  36222  eqlkr  36250  lkrlsp  36253  atcvrj2b  36583  3dim1  36618  3dim2  36619  llni2  36663  2llnjaN  36717  lvoli3  36728  lvoli2  36732  lncvrelatN  36932  lhpat4N  37195  lhpat3  37197  4atexlemex6  37225  ldilco  37267  ltrnid  37286  ltrnatb  37288  ltrnel  37290  ltrncnvel  37293  ltrncnv  37297  ltrn11at  37298  ltrneq  37300  trlat  37320  trlator0  37322  ltrnnidn  37325  trlid0  37327  trlnidatb  37328  trlnle  37337  trlval3  37338  trlval4  37339  cdlemc2  37343  cdlemc5  37346  cdlemc6  37347  cdlemc  37348  cdlemd2  37350  cdlemd9  37357  cdleme0e  37368  cdleme02N  37373  cdleme0ex1N  37374  cdleme3e  37383  cdleme3g  37385  cdleme3h  37386  cdleme3  37388  cdleme7aa  37393  cdleme7b  37395  cdleme7c  37396  cdleme7d  37397  cdleme7e  37398  cdleme7ga  37399  cdleme7  37400  cdleme9  37404  cdleme16aN  37410  cdleme11c  37412  cdleme11dN  37413  cdleme11e  37414  cdleme11h  37417  cdleme11j  37418  cdleme11k  37419  cdleme12  37422  cdleme21j  37487  cdleme26eALTN  37512  cdleme26f  37514  cdleme26f2  37516  cdlemefrs29bpre0  37547  cdleme35a  37599  cdleme35b  37601  cdleme35c  37602  cdleme35f  37605  cdleme36a  37611  cdleme38m  37614  cdlemeg46rgv  37679  cdlemeg46req  37680  cdlemf  37714  cdlemg2fvlem  37745  cdlemg2l  37754  cdlemg7N  37777  cdlemg12g  37800  cdlemg15  37807  cdlemg17h  37819  cdlemg17  37828  cdlemg19a  37834  cdlemg24  37839  cdlemg37  37840  cdlemg27a  37843  cdlemg31b0N  37845  cdlemg27b  37847  cdlemg31c  37850  cdlemg31d  37851  cdlemg35  37864  trljco  37891  tgrpgrplem  37900  cdlemh2  37967  tendoconid  37980  tendotr  37981  cdlemk35s-id  38089  cdlemk39s-id  38091  cdlemk53b  38107  cdlemk53  38108  cdlemk54  38109  cdleml3N  38129  cdleml5N  38131  tendospcanN  38174  diclss  38344  dihvalcq2  38398  dihord4  38409  dihord5b  38410  dihord5apre  38413  dihmeetlem1N  38441  dihmeetbclemN  38455  dihmeetlem20N  38477  dihmeetALTN  38478  dihatlat  38485  dihatexv  38489  dochkr1  38629  dochkr1OLDN  38630  lcfl7lem  38650  lclkrlem2m  38670  hdmaplna1  39058  hdmaplns1  39059  hdmaplnm1  39060  eldioph2lem1  39406  fphpdo  39463  irrapxlem1  39468  irrapxlem2  39469  irrapxlem3  39470  irrapxlem5  39472  pellexlem2  39476  pell1234qrreccl  39500  pell1234qrmulcl  39501  pell1234qrdich  39507  pell1qr1  39517  pellqrexplicit  39523  pellfundex  39532  reglogltb  39537  reglogleb  39538  pellfund14  39544  rmxycomplete  39563  jm2.24nn  39605  jm2.17b  39607  jm2.17c  39608  jm2.18  39634  jm2.19lem2  39636  jm2.20nn  39643  jm2.16nn0  39650  jm3.1lem2  39664  areaquad  39872  clsk3nimkb  40439  lemuldiv3d  40571  lemuldiv4d  40572  stoweidlem1  42335  stoweidlem11  42345  stoweidlem14  42348  stoweidlem26  42360  stoweidlem34  42368  stoweidlem38  42372  stoweidlem60  42394  fourierdlem52  42492  etransclem38  42606  reuopreuprim  43737  quad1  43834  requad1  43836  requad2  43837  domnmsuppn0  44466  lincvalpr  44522  ldepspr  44577  islindeps2  44587  fldivexpfllog2  44674  eenglngeehlnmlem1  44773  eenglngeehlnmlem2  44774  rrx2linest  44778