Theorem syl112anc 1375

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 1372	1 ⊢ (𝜑 → 𝜂)

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

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 1090

This theorem is referenced by:  rmob2  3886  2nreu  4441  fveqf1o  7298  frrlem12  8279  enfixsn  9078  gruina  10810  grur1  10812  enqeq  10926  recrec  11908  rec11r  11910  divdivdiv  11912  dmdcan  11921  ddcan  11925  rereccl  11929  div2neg  11934  divmuld  12009  divmul2d  12020  divmul3d  12021  divassd  12022  div12d  12023  div23d  12024  divdird  12025  divsubdird  12026  div11d  12027  ltmul12a  12067  ltdiv1  12075  ltrec  12093  lt2msq1  12095  lediv2  12101  supmul1  12180  qbtwnre  13175  xlemul1a  13264  xlemul1  13266  xadd4d  13279  quoremz  13817  quoremnn0ALT  13819  expgt1  14063  nnlesq  14166  expnbnd  14192  expmulnbnd  14195  discr1  14199  facubnd  14257  pfxsuffeqwrdeq  14645  01sqrexlem6  15191  mulcn2  15537  geomulcvg  15819  cvgrat  15826  eftlub  16049  eflegeo  16061  tanhlt1  16100  sin01bnd  16125  cos01bnd  16126  eirrlem  16144  bitsmod  16374  mulgcd  16487  mulgcddvds  16589  prmind2  16619  qnumgt0  16683  pcpremul  16773  fldivp1  16827  pcfaclem  16828  qexpz  16831  prmpwdvds  16834  pockthg  16836  prmreclem1  16846  prmreclem5  16850  4sqlem10  16877  4sqlem12  16886  4sqlem16  16890  4sqlem17  16891  vdwlem3  16913  vdwlem8  16918  vdwlem9  16919  0ram  16950  ramz2  16954  cat1lem  18043  odmulg  19419  dfod2  19427  odf1o1  19435  odf1o2  19436  sylow3lem4  19493  ablsub4  19673  odadd1  19711  odadd2  19712  ablfacrp2  19932  ablfac1b  19935  ablfac1eu  19938  pgpfac1lem3a  19941  pgpfaclem2  19947  ablsimpgfindlem1  19972  chrcong  21073  znrrg  21113  cygznlem1  21114  chpdmatlem3  22334  txdis  23128  txdis1cn  23131  ptunhmeo  23304  qustgplem  23617  blcld  24006  nlmvscnlem2  24194  blcvx  24306  metds0  24358  metdseq0  24362  icopnfcnv  24450  lebnumii  24474  ipcau2  24743  tcphcphlem1  24744  ipcnlem2  24753  csbren  24908  trirn  24909  dyadf  25100  dyadovol  25102  dyaddisjlem  25104  dyadmaxlem  25106  opnmbllem  25110  mbfmulc2lem  25156  mbfi1fseqlem4  25228  mbfi1fseqlem5  25229  mbfi1fseqlem6  25230  itg2mulclem  25256  itg2monolem1  25260  itg2monolem3  25262  itg2cnlem2  25272  itgabs  25344  dvlip  25502  dvlt0  25514  dvcvx  25529  ftc1lem4  25548  dgrcolem2  25780  aaliou3lem2  25848  aaliou3lem9  25855  itgulm  25912  radcnvlem1  25917  abelthlem2  25936  abelthlem7  25942  tangtx  26007  cosne0  26030  cosordlem  26031  tanord1  26038  logdivlti  26120  logcnlem4  26145  logf1o2  26150  cxpcn3lem  26245  cxpaddle  26250  ang180lem2  26305  atanlogsublem  26410  atantan  26418  atanbndlem  26420  atans2  26426  leibpi  26437  log2tlbnd  26440  birthdaylem3  26448  efrlim  26464  jensenlem2  26482  zetacvg  26509  ftalem1  26567  ftalem5  26571  basellem1  26575  basellem4  26578  fsumdvdsdiaglem  26677  dvdsflf1o  26681  fsumfldivdiaglem  26683  ppiub  26697  mersenne  26720  dchrptlem1  26757  bposlem1  26777  bposlem2  26778  bposlem4  26780  lgsdilem  26817  lgseisenlem1  26868  lgseisenlem2  26869  lgseisenlem3  26870  lgsquadlem1  26873  lgsquadlem2  26874  2sqlem3  26913  2sqlem8  26919  2sqlem11  26922  2sqblem  26924  chebbnd1lem2  26963  chebbnd1lem3  26964  rplogsumlem1  26977  rplogsumlem2  26978  dchrisumlem1  26982  dchrmusum2  26987  dchrisum0flblem1  27001  mulog2sumlem1  27027  logdivbnd  27049  pntpbnd1a  27078  pntpbnd1  27079  pntpbnd2  27080  pntlemh  27092  pntlemr  27095  pntlemk  27099  pntlemo  27100  ostth2lem1  27111  ostth2lem2  27127  ostth2lem3  27128  ostth3  27131  noextenddif  27161  noextendlt  27162  noextendgt  27163  nosupbnd1lem3  27203  nosupbnd1lem4  27204  nosupbnd1lem5  27205  nosupbnd1lem6  27206  noinfbnd1lem3  27218  noinfbnd1lem4  27219  noinfbnd1lem5  27220  noinfbnd1lem6  27221  noetasuplem4  27229  madecut  27367  cofcut2  27399  legov  27826  axsegcon  28175  axpaschlem  28188  0uhgrsubgr  28526  clwwlkf1  29292  upgr4cycl4dv4e  29428  eupth2lem3lem3  29473  nmblolbii  30040  nmbdoplbi  31265  nmcoplbi  31269  nmophmi  31272  nmbdfnlbi  31290  nmcfnlbi  31293  cnlnadjlem7  31314  nmopcoi  31336  resf1o  31943  xdivrec  32081  cycpmfvlem  32259  cycpmfv3  32262  lbsdiflsp0  32700  txomap  32803  unitdivcld  32870  measvunilem  33199  measvuni  33201  measssd  33202  measiuns  33204  measinblem  33207  measdivcst  33211  sibfof  33328  oddpwdc  33342  sseqfv1  33377  sseqfv2  33382  probun  33407  totprobd  33414  dstrvprob  33459  actfunsnrndisj  33606  reprsuc  33616  breprexplema  33631  subfaclim  34168  connpconn  34215  cvmliftlem2  34266  cvmliftlem6  34270  cvmliftlem7  34271  cvmliftlem8  34272  cvmliftlem9  34273  cvmliftlem10  34274  snmlff  34309  lineext  35037  hilbert1.1  35115  nn0prpwlem  35196  poimirlem1  36478  opnmbllem0  36513  ismblfin  36518  itgabsnc  36546  ftc1cnnclem  36548  bfplem1  36679  bfp  36681  lfl1  37929  lfladdcl  37930  eqlkr  37958  lkrlsp  37961  atcvrj2b  38292  3dim1  38327  3dim2  38328  llni2  38372  2llnjaN  38426  lvoli3  38437  lvoli2  38441  lncvrelatN  38641  lhpat4N  38904  lhpat3  38906  4atexlemex6  38934  ldilco  38976  ltrnid  38995  ltrnatb  38997  ltrnel  38999  ltrncnvel  39002  ltrncnv  39006  ltrn11at  39007  ltrneq  39009  trlat  39029  trlator0  39031  ltrnnidn  39034  trlid0  39036  trlnidatb  39037  trlnle  39046  trlval3  39047  trlval4  39048  cdlemc2  39052  cdlemc5  39055  cdlemc6  39056  cdlemc  39057  cdlemd2  39059  cdlemd9  39066  cdleme0e  39077  cdleme02N  39082  cdleme0ex1N  39083  cdleme3e  39092  cdleme3g  39094  cdleme3h  39095  cdleme3  39097  cdleme7aa  39102  cdleme7b  39104  cdleme7c  39105  cdleme7d  39106  cdleme7e  39107  cdleme7ga  39108  cdleme7  39109  cdleme9  39113  cdleme16aN  39119  cdleme11c  39121  cdleme11dN  39122  cdleme11e  39123  cdleme11h  39126  cdleme11j  39127  cdleme11k  39128  cdleme12  39131  cdleme21j  39196  cdleme26eALTN  39221  cdleme26f  39223  cdleme26f2  39225  cdlemefrs29bpre0  39256  cdleme35a  39308  cdleme35b  39310  cdleme35c  39311  cdleme35f  39314  cdleme36a  39320  cdleme38m  39323  cdlemeg46rgv  39388  cdlemeg46req  39389  cdlemf  39423  cdlemg2fvlem  39454  cdlemg2l  39463  cdlemg7N  39486  cdlemg12g  39509  cdlemg15  39516  cdlemg17h  39528  cdlemg17  39537  cdlemg19a  39543  cdlemg24  39548  cdlemg37  39549  cdlemg27a  39552  cdlemg31b0N  39554  cdlemg27b  39556  cdlemg31c  39559  cdlemg31d  39560  cdlemg35  39573  trljco  39600  tgrpgrplem  39609  cdlemh2  39676  tendoconid  39689  tendotr  39690  cdlemk35s-id  39798  cdlemk39s-id  39800  cdlemk53b  39816  cdlemk53  39817  cdlemk54  39818  cdleml3N  39838  cdleml5N  39840  tendospcanN  39883  diclss  40053  dihvalcq2  40107  dihord4  40118  dihord5b  40119  dihord5apre  40122  dihmeetlem1N  40150  dihmeetbclemN  40164  dihmeetlem20N  40186  dihmeetALTN  40187  dihatlat  40194  dihatexv  40198  dochkr1  40338  dochkr1OLDN  40339  lcfl7lem  40359  lclkrlem2m  40379  hdmaplna1  40767  hdmaplns1  40768  hdmaplnm1  40769  eldioph2lem1  41484  fphpdo  41541  irrapxlem1  41546  irrapxlem2  41547  irrapxlem3  41548  irrapxlem5  41550  pellexlem2  41554  pell1234qrreccl  41578  pell1234qrmulcl  41579  pell1234qrdich  41585  pell1qr1  41595  pellqrexplicit  41601  pellfundex  41610  reglogltb  41615  reglogleb  41616  pellfund14  41622  rmxycomplete  41642  jm2.24nn  41684  jm2.17b  41686  jm2.17c  41687  jm2.18  41713  jm2.19lem2  41715  jm2.20nn  41722  jm2.16nn0  41729  jm3.1lem2  41743  areaquad  41951  clsk3nimkb  42777  lemuldiv3d  42908  lemuldiv4d  42909  stoweidlem1  44704  stoweidlem11  44714  stoweidlem14  44717  stoweidlem26  44729  stoweidlem34  44737  stoweidlem38  44741  stoweidlem60  44763  fourierdlem52  44861  etransclem38  44975  reuopreuprim  46181  quad1  46275  requad1  46277  requad2  46278  domnmsuppn0  46999  lincvalpr  47053  ldepspr  47108  islindeps2  47118  fldivexpfllog2  47205  eenglngeehlnmlem1  47377  eenglngeehlnmlem2  47378  rrx2linest  47382  prsthinc  47628