Theorem syl112anc 1382

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  rmob2  3831  2nreu  4379  fveqf1o  7253  frrlem12  8244  enfixsn  9021  gruina  10739  grur1  10741  enqeq  10855  muldivdid  11847  recrec  11850  rec11r  11852  divdivdiv  11854  dmdcan  11863  ddcan  11867  rereccl  11871  div2neg  11876  divmuld  11951  divmul2d  11962  divmul3d  11963  divassd  11964  div12d  11965  div23d  11966  divdird  11967  divsubdird  11968  div11d  11969  ltmul12a  12009  ltdiv1  12018  ltrec  12036  lt2msq1  12038  lediv2  12044  supmul1  12123  qbtwnre  13149  xlemul1a  13238  xlemul1  13240  xadd4d  13253  quoremz  13812  quoremnn0ALT  13814  expgt1  14060  nnlesq  14165  expnbnd  14192  expmulnbnd  14195  discr1  14199  facubnd  14260  pfxsuffeqwrdeq  14658  01sqrexlem6  15207  mulcn2  15556  geomulcvg  15839  cvgrat  15846  eftlub  16074  eflegeo  16086  tanhlt1  16125  sin01bnd  16150  cos01bnd  16151  eirrlem  16169  bitsmod  16403  mulgcd  16515  mulgcddvds  16622  prmind2  16652  qnumgt0  16718  pcpremul  16812  fldivp1  16866  pcfaclem  16867  qexpz  16870  prmpwdvds  16873  pockthg  16875  prmreclem1  16885  prmreclem5  16889  4sqlem10  16916  4sqlem12  16925  4sqlem16  16929  4sqlem17  16930  vdwlem3  16952  vdwlem8  16957  vdwlem9  16958  0ram  16989  ramz2  16993  cat1lem  18061  odmulg  19529  dfod2  19537  odf1o1  19545  odf1o2  19546  sylow3lem4  19603  ablsub4  19783  odadd1  19821  odadd2  19822  ablfacrp2  20042  ablfac1b  20045  ablfac1eu  20048  pgpfac1lem3a  20051  pgpfaclem2  20057  ablsimpgfindlem1  20082  chrcong  21509  znrrg  21547  cygznlem1  21548  chpdmatlem3  22830  txdis  23622  txdis1cn  23625  ptunhmeo  23798  qustgplem  24111  blcld  24495  nlmvscnlem2  24675  blcvx  24788  metds0  24841  metdseq0  24845  icopnfcnv  24934  lebnumii  24958  ipcau2  25226  tcphcphlem1  25227  ipcnlem2  25236  csbren  25391  trirn  25392  dyadf  25583  dyadovol  25585  dyaddisjlem  25587  dyadmaxlem  25589  opnmbllem  25593  mbfmulc2lem  25639  mbfi1fseqlem4  25710  mbfi1fseqlem5  25711  mbfi1fseqlem6  25712  itg2mulclem  25738  itg2monolem1  25742  itg2monolem3  25744  itg2cnlem2  25754  itgabs  25827  dvlip  25985  dvlt0  25997  dvcvx  26012  ftc1lem4  26031  dgrcolem2  26264  aaliou3lem2  26334  aaliou3lem9  26341  itgulm  26398  radcnvlem1  26403  abelthlem2  26422  abelthlem7  26428  tangtx  26494  cosne0  26518  cosordlem  26519  tanord1  26526  logdivlti  26609  logcnlem4  26634  logf1o2  26639  cxpcn3lem  26736  cxpaddle  26741  ang180lem2  26799  atanlogsublem  26904  atantan  26912  atanbndlem  26914  atans2  26920  leibpi  26931  log2tlbnd  26934  birthdaylem3  26942  efrlim  26958  jensenlem2  26976  zetacvg  27003  ftalem1  27061  ftalem5  27065  basellem1  27069  basellem4  27072  fsumdvdsdiaglem  27171  dvdsflf1o  27175  fsumfldivdiaglem  27177  ppiub  27192  mersenne  27215  dchrptlem1  27252  bposlem1  27272  bposlem2  27273  bposlem4  27275  lgsdilem  27312  lgseisenlem1  27363  lgseisenlem2  27364  lgseisenlem3  27365  lgsquadlem1  27368  lgsquadlem2  27369  2sqlem3  27408  2sqlem8  27414  2sqlem11  27417  2sqblem  27419  chebbnd1lem2  27458  chebbnd1lem3  27459  rplogsumlem1  27472  rplogsumlem2  27473  dchrisumlem1  27477  dchrmusum2  27482  dchrisum0flblem1  27496  mulog2sumlem1  27522  logdivbnd  27544  pntpbnd1a  27573  pntpbnd1  27574  pntpbnd2  27575  pntlemh  27587  pntlemr  27590  pntlemk  27594  pntlemo  27595  ostth2lem1  27606  ostth2lem2  27622  ostth2lem3  27623  ostth3  27626  noextenddif  27657  noextendlt  27658  noextendgt  27659  nosupbnd1lem3  27699  nosupbnd1lem4  27700  nosupbnd1lem5  27701  nosupbnd1lem6  27702  noinfbnd1lem3  27714  noinfbnd1lem4  27715  noinfbnd1lem5  27716  noinfbnd1lem6  27717  noetasuplem4  27725  madecut  27900  cofcut2  27939  eucliddivs  28393  legov  28678  axsegcon  29021  axpaschlem  29034  0uhgrsubgr  29373  clwwlkf1  30144  upgr4cycl4dv4e  30280  eupth2lem3lem3  30325  nrt2irr  30568  nmblolbii  30895  nmbdoplbi  32120  nmcoplbi  32124  nmophmi  32127  nmbdfnlbi  32145  nmcfnlbi  32148  cnlnadjlem7  32169  nmopcoi  32191  resf1o  32829  receqid  32843  xdivrec  33012  cycpmfvlem  33200  cycpmfv3  33203  lbsdiflsp0  33817  txomap  34025  unitdivcld  34092  measvunilem  34403  measvuni  34405  measssd  34406  measiuns  34408  measinblem  34411  measdivcst  34415  sibfof  34531  oddpwdc  34545  sseqfv1  34580  sseqfv2  34585  probun  34610  totprobd  34617  dstrvprob  34663  actfunsnrndisj  34796  reprsuc  34806  breprexplema  34821  subfaclim  35423  connpconn  35470  cvmliftlem2  35521  cvmliftlem6  35525  cvmliftlem7  35526  cvmliftlem8  35527  cvmliftlem9  35528  cvmliftlem10  35529  snmlff  35564  lineext  36311  hilbert1.1  36389  nn0prpwlem  36557  poimirlem1  37995  opnmbllem0  38030  ismblfin  38035  itgabsnc  38063  ftc1cnnclem  38065  bfplem1  38196  bfp  38198  lfl1  39569  lfladdcl  39570  eqlkr  39598  lkrlsp  39601  atcvrj2b  39931  3dim1  39966  3dim2  39967  llni2  40011  2llnjaN  40065  lvoli3  40076  lvoli2  40080  lncvrelatN  40280  lhpat4N  40543  lhpat3  40545  4atexlemex6  40573  ldilco  40615  ltrnid  40634  ltrnatb  40636  ltrnel  40638  ltrncnvel  40641  ltrncnv  40645  ltrn11at  40646  ltrneq  40648  trlat  40668  trlator0  40670  ltrnnidn  40673  trlid0  40675  trlnidatb  40676  trlnle  40685  trlval3  40686  trlval4  40687  cdlemc2  40691  cdlemc5  40694  cdlemc6  40695  cdlemc  40696  cdlemd2  40698  cdlemd9  40705  cdleme0e  40716  cdleme02N  40721  cdleme0ex1N  40722  cdleme3e  40731  cdleme3g  40733  cdleme3h  40734  cdleme3  40736  cdleme7aa  40741  cdleme7b  40743  cdleme7c  40744  cdleme7d  40745  cdleme7e  40746  cdleme7ga  40747  cdleme7  40748  cdleme9  40752  cdleme16aN  40758  cdleme11c  40760  cdleme11dN  40761  cdleme11e  40762  cdleme11h  40765  cdleme11j  40766  cdleme11k  40767  cdleme12  40770  cdleme21j  40835  cdleme26eALTN  40860  cdleme26f  40862  cdleme26f2  40864  cdlemefrs29bpre0  40895  cdleme35a  40947  cdleme35b  40949  cdleme35c  40950  cdleme35f  40953  cdleme36a  40959  cdleme38m  40962  cdlemeg46rgv  41027  cdlemeg46req  41028  cdlemf  41062  cdlemg2fvlem  41093  cdlemg2l  41102  cdlemg7N  41125  cdlemg12g  41148  cdlemg15  41155  cdlemg17h  41167  cdlemg17  41176  cdlemg19a  41182  cdlemg24  41187  cdlemg37  41188  cdlemg27a  41191  cdlemg31b0N  41193  cdlemg27b  41195  cdlemg31c  41198  cdlemg31d  41199  cdlemg35  41212  trljco  41239  tgrpgrplem  41248  cdlemh2  41315  tendoconid  41328  tendotr  41329  cdlemk35s-id  41437  cdlemk39s-id  41439  cdlemk53b  41455  cdlemk53  41456  cdlemk54  41457  cdleml3N  41477  cdleml5N  41479  tendospcanN  41522  diclss  41692  dihvalcq2  41746  dihord4  41757  dihord5b  41758  dihord5apre  41761  dihmeetlem1N  41789  dihmeetbclemN  41803  dihmeetlem20N  41825  dihmeetALTN  41826  dihatlat  41833  dihatexv  41837  dochkr1  41977  dochkr1OLDN  41978  lcfl7lem  41998  lclkrlem2m  42018  hdmaplna1  42406  hdmaplns1  42407  hdmaplnm1  42408  cxp111d  42826  eldioph2lem1  43216  fphpdo  43269  irrapxlem1  43274  irrapxlem2  43275  irrapxlem3  43276  irrapxlem5  43278  pellexlem2  43282  pell1234qrreccl  43306  pell1234qrmulcl  43307  pell1234qrdich  43313  pell1qr1  43323  pellqrexplicit  43329  pellfundex  43338  reglogltb  43343  reglogleb  43344  pellfund14  43350  rmxycomplete  43369  jm2.24nn  43411  jm2.17b  43413  jm2.17c  43414  jm2.18  43440  jm2.19lem2  43442  jm2.20nn  43449  jm2.16nn0  43456  jm3.1lem2  43470  areaquad  43668  clsk3nimkb  44491  lemuldiv3d  44621  lemuldiv4d  44622  stoweidlem1  46451  stoweidlem11  46461  stoweidlem14  46464  stoweidlem26  46476  stoweidlem34  46484  stoweidlem38  46488  stoweidlem60  46510  fourierdlem52  46608  etransclem38  46722  2tceilhalfelfzo1  47806  reuopreuprim  48008  nprmdvdsfacm1lem4  48108  quad1  48118  requad1  48120  requad2  48121  isubgr3stgrlem1  48464  isubgr3stgrlem3  48466  gpg3kgrtriexlem1  48581  gpg3kgrtriexlem5  48585  domnmsuppn0  48867  lincvalpr  48916  ldepspr  48971  islindeps2  48981  fldivexpfllog2  49063  eenglngeehlnmlem1  49235  eenglngeehlnmlem2  49236  rrx2linest  49240  prsthinc  49961