Theorem syl112anc 1377

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ 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 207  df-an 396  df-3an 1089

This theorem is referenced by:  rmob2  3830  2nreu  4384  fveqf1o  7257  frrlem12  8247  enfixsn  9024  gruina  10741  grur1  10743  enqeq  10857  muldivdid  11849  recrec  11852  rec11r  11854  divdivdiv  11856  dmdcan  11865  ddcan  11869  rereccl  11873  div2neg  11878  divmuld  11953  divmul2d  11964  divmul3d  11965  divassd  11966  div12d  11967  div23d  11968  divdird  11969  divsubdird  11970  div11d  11971  ltmul12a  12011  ltdiv1  12020  ltrec  12038  lt2msq1  12040  lediv2  12046  supmul1  12125  qbtwnre  13151  xlemul1a  13240  xlemul1  13242  xadd4d  13255  quoremz  13814  quoremnn0ALT  13816  expgt1  14062  nnlesq  14167  expnbnd  14194  expmulnbnd  14197  discr1  14201  facubnd  14262  pfxsuffeqwrdeq  14660  01sqrexlem6  15209  mulcn2  15558  geomulcvg  15841  cvgrat  15848  eftlub  16076  eflegeo  16088  tanhlt1  16127  sin01bnd  16152  cos01bnd  16153  eirrlem  16171  bitsmod  16405  mulgcd  16517  mulgcddvds  16624  prmind2  16654  qnumgt0  16720  pcpremul  16814  fldivp1  16868  pcfaclem  16869  qexpz  16872  prmpwdvds  16875  pockthg  16877  prmreclem1  16887  prmreclem5  16891  4sqlem10  16918  4sqlem12  16927  4sqlem16  16931  4sqlem17  16932  vdwlem3  16954  vdwlem8  16959  vdwlem9  16960  0ram  16991  ramz2  16995  cat1lem  18063  odmulg  19531  dfod2  19539  odf1o1  19547  odf1o2  19548  sylow3lem4  19605  ablsub4  19785  odadd1  19823  odadd2  19824  ablfacrp2  20044  ablfac1b  20047  ablfac1eu  20050  pgpfac1lem3a  20053  pgpfaclem2  20059  ablsimpgfindlem1  20084  chrcong  21507  znrrg  21545  cygznlem1  21546  chpdmatlem3  22805  txdis  23597  txdis1cn  23600  ptunhmeo  23773  qustgplem  24086  blcld  24470  nlmvscnlem2  24650  blcvx  24763  metds0  24816  metdseq0  24820  icopnfcnv  24909  lebnumii  24933  ipcau2  25201  tcphcphlem1  25202  ipcnlem2  25211  csbren  25366  trirn  25367  dyadf  25558  dyadovol  25560  dyaddisjlem  25562  dyadmaxlem  25564  opnmbllem  25568  mbfmulc2lem  25614  mbfi1fseqlem4  25685  mbfi1fseqlem5  25686  mbfi1fseqlem6  25687  itg2mulclem  25713  itg2monolem1  25717  itg2monolem3  25719  itg2cnlem2  25729  itgabs  25802  dvlip  25960  dvlt0  25972  dvcvx  25987  ftc1lem4  26006  dgrcolem2  26239  aaliou3lem2  26309  aaliou3lem9  26316  itgulm  26373  radcnvlem1  26378  abelthlem2  26397  abelthlem7  26403  tangtx  26469  cosne0  26493  cosordlem  26494  tanord1  26501  logdivlti  26584  logcnlem4  26609  logf1o2  26614  cxpcn3lem  26711  cxpaddle  26716  ang180lem2  26774  atanlogsublem  26879  atantan  26887  atanbndlem  26889  atans2  26895  leibpi  26906  log2tlbnd  26909  birthdaylem3  26917  efrlim  26933  jensenlem2  26951  zetacvg  26978  ftalem1  27036  ftalem5  27040  basellem1  27044  basellem4  27047  fsumdvdsdiaglem  27146  dvdsflf1o  27150  fsumfldivdiaglem  27152  ppiub  27167  mersenne  27190  dchrptlem1  27227  bposlem1  27247  bposlem2  27248  bposlem4  27250  lgsdilem  27287  lgseisenlem1  27338  lgseisenlem2  27339  lgseisenlem3  27340  lgsquadlem1  27343  lgsquadlem2  27344  2sqlem3  27383  2sqlem8  27389  2sqlem11  27392  2sqblem  27394  chebbnd1lem2  27433  chebbnd1lem3  27434  rplogsumlem1  27447  rplogsumlem2  27448  dchrisumlem1  27452  dchrmusum2  27457  dchrisum0flblem1  27471  mulog2sumlem1  27497  logdivbnd  27519  pntpbnd1a  27548  pntpbnd1  27549  pntpbnd2  27550  pntlemh  27562  pntlemr  27565  pntlemk  27569  pntlemo  27570  ostth2lem1  27581  ostth2lem2  27597  ostth2lem3  27598  ostth3  27601  noextenddif  27632  noextendlt  27633  noextendgt  27634  nosupbnd1lem3  27674  nosupbnd1lem4  27675  nosupbnd1lem5  27676  nosupbnd1lem6  27677  noinfbnd1lem3  27689  noinfbnd1lem4  27690  noinfbnd1lem5  27691  noinfbnd1lem6  27692  noetasuplem4  27700  madecut  27875  cofcut2  27914  eucliddivs  28368  legov  28653  axsegcon  28996  axpaschlem  29009  0uhgrsubgr  29348  clwwlkf1  30119  upgr4cycl4dv4e  30255  eupth2lem3lem3  30300  nrt2irr  30543  nmblolbii  30870  nmbdoplbi  32095  nmcoplbi  32099  nmophmi  32102  nmbdfnlbi  32120  nmcfnlbi  32123  cnlnadjlem7  32144  nmopcoi  32166  resf1o  32803  receqid  32817  xdivrec  32986  cycpmfvlem  33173  cycpmfv3  33176  lbsdiflsp0  33770  txomap  33978  unitdivcld  34045  measvunilem  34356  measvuni  34358  measssd  34359  measiuns  34361  measinblem  34364  measdivcst  34368  sibfof  34484  oddpwdc  34498  sseqfv1  34533  sseqfv2  34538  probun  34563  totprobd  34570  dstrvprob  34616  actfunsnrndisj  34749  reprsuc  34759  breprexplema  34774  subfaclim  35370  connpconn  35417  cvmliftlem2  35468  cvmliftlem6  35472  cvmliftlem7  35473  cvmliftlem8  35474  cvmliftlem9  35475  cvmliftlem10  35476  snmlff  35511  lineext  36258  hilbert1.1  36336  nn0prpwlem  36504  poimirlem1  37942  opnmbllem0  37977  ismblfin  37982  itgabsnc  38010  ftc1cnnclem  38012  bfplem1  38143  bfp  38145  lfl1  39516  lfladdcl  39517  eqlkr  39545  lkrlsp  39548  atcvrj2b  39878  3dim1  39913  3dim2  39914  llni2  39958  2llnjaN  40012  lvoli3  40023  lvoli2  40027  lncvrelatN  40227  lhpat4N  40490  lhpat3  40492  4atexlemex6  40520  ldilco  40562  ltrnid  40581  ltrnatb  40583  ltrnel  40585  ltrncnvel  40588  ltrncnv  40592  ltrn11at  40593  ltrneq  40595  trlat  40615  trlator0  40617  ltrnnidn  40620  trlid0  40622  trlnidatb  40623  trlnle  40632  trlval3  40633  trlval4  40634  cdlemc2  40638  cdlemc5  40641  cdlemc6  40642  cdlemc  40643  cdlemd2  40645  cdlemd9  40652  cdleme0e  40663  cdleme02N  40668  cdleme0ex1N  40669  cdleme3e  40678  cdleme3g  40680  cdleme3h  40681  cdleme3  40683  cdleme7aa  40688  cdleme7b  40690  cdleme7c  40691  cdleme7d  40692  cdleme7e  40693  cdleme7ga  40694  cdleme7  40695  cdleme9  40699  cdleme16aN  40705  cdleme11c  40707  cdleme11dN  40708  cdleme11e  40709  cdleme11h  40712  cdleme11j  40713  cdleme11k  40714  cdleme12  40717  cdleme21j  40782  cdleme26eALTN  40807  cdleme26f  40809  cdleme26f2  40811  cdlemefrs29bpre0  40842  cdleme35a  40894  cdleme35b  40896  cdleme35c  40897  cdleme35f  40900  cdleme36a  40906  cdleme38m  40909  cdlemeg46rgv  40974  cdlemeg46req  40975  cdlemf  41009  cdlemg2fvlem  41040  cdlemg2l  41049  cdlemg7N  41072  cdlemg12g  41095  cdlemg15  41102  cdlemg17h  41114  cdlemg17  41123  cdlemg19a  41129  cdlemg24  41134  cdlemg37  41135  cdlemg27a  41138  cdlemg31b0N  41140  cdlemg27b  41142  cdlemg31c  41145  cdlemg31d  41146  cdlemg35  41159  trljco  41186  tgrpgrplem  41195  cdlemh2  41262  tendoconid  41275  tendotr  41276  cdlemk35s-id  41384  cdlemk39s-id  41386  cdlemk53b  41402  cdlemk53  41403  cdlemk54  41404  cdleml3N  41424  cdleml5N  41426  tendospcanN  41469  diclss  41639  dihvalcq2  41693  dihord4  41704  dihord5b  41705  dihord5apre  41708  dihmeetlem1N  41736  dihmeetbclemN  41750  dihmeetlem20N  41772  dihmeetALTN  41773  dihatlat  41780  dihatexv  41784  dochkr1  41924  dochkr1OLDN  41925  lcfl7lem  41945  lclkrlem2m  41965  hdmaplna1  42353  hdmaplns1  42354  hdmaplnm1  42355  cxp111d  42774  eldioph2lem1  43192  fphpdo  43245  irrapxlem1  43250  irrapxlem2  43251  irrapxlem3  43252  irrapxlem5  43254  pellexlem2  43258  pell1234qrreccl  43282  pell1234qrmulcl  43283  pell1234qrdich  43289  pell1qr1  43299  pellqrexplicit  43305  pellfundex  43314  reglogltb  43319  reglogleb  43320  pellfund14  43326  rmxycomplete  43345  jm2.24nn  43387  jm2.17b  43389  jm2.17c  43390  jm2.18  43416  jm2.19lem2  43418  jm2.20nn  43425  jm2.16nn0  43432  jm3.1lem2  43446  areaquad  43644  clsk3nimkb  44467  lemuldiv3d  44597  lemuldiv4d  44598  stoweidlem1  46429  stoweidlem11  46439  stoweidlem14  46442  stoweidlem26  46454  stoweidlem34  46462  stoweidlem38  46466  stoweidlem60  46488  fourierdlem52  46586  etransclem38  46700  2tceilhalfelfzo1  47784  reuopreuprim  47986  nprmdvdsfacm1lem4  48086  quad1  48096  requad1  48098  requad2  48099  isubgr3stgrlem1  48442  isubgr3stgrlem3  48444  gpg3kgrtriexlem1  48559  gpg3kgrtriexlem5  48563  domnmsuppn0  48845  lincvalpr  48894  ldepspr  48949  islindeps2  48959  fldivexpfllog2  49041  eenglngeehlnmlem1  49213  eenglngeehlnmlem2  49214  rrx2linest  49218  prsthinc  49939