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  3831  2nreu  4385  fveqf1o  7250  frrlem12  8240  enfixsn  9017  gruina  10732  grur1  10734  enqeq  10848  muldivdid  11840  recrec  11843  rec11r  11845  divdivdiv  11847  dmdcan  11856  ddcan  11860  rereccl  11864  div2neg  11869  divmuld  11944  divmul2d  11955  divmul3d  11956  divassd  11957  div12d  11958  div23d  11959  divdird  11960  divsubdird  11961  div11d  11962  ltmul12a  12002  ltdiv1  12011  ltrec  12029  lt2msq1  12031  lediv2  12037  supmul1  12116  qbtwnre  13142  xlemul1a  13231  xlemul1  13233  xadd4d  13246  quoremz  13805  quoremnn0ALT  13807  expgt1  14053  nnlesq  14158  expnbnd  14185  expmulnbnd  14188  discr1  14192  facubnd  14253  pfxsuffeqwrdeq  14651  01sqrexlem6  15200  mulcn2  15549  geomulcvg  15832  cvgrat  15839  eftlub  16067  eflegeo  16079  tanhlt1  16118  sin01bnd  16143  cos01bnd  16144  eirrlem  16162  bitsmod  16396  mulgcd  16508  mulgcddvds  16615  prmind2  16645  qnumgt0  16711  pcpremul  16805  fldivp1  16859  pcfaclem  16860  qexpz  16863  prmpwdvds  16866  pockthg  16868  prmreclem1  16878  prmreclem5  16882  4sqlem10  16909  4sqlem12  16918  4sqlem16  16922  4sqlem17  16923  vdwlem3  16945  vdwlem8  16950  vdwlem9  16951  0ram  16982  ramz2  16986  cat1lem  18054  odmulg  19522  dfod2  19530  odf1o1  19538  odf1o2  19539  sylow3lem4  19596  ablsub4  19776  odadd1  19814  odadd2  19815  ablfacrp2  20035  ablfac1b  20038  ablfac1eu  20041  pgpfac1lem3a  20044  pgpfaclem2  20050  ablsimpgfindlem1  20075  chrcong  21517  znrrg  21555  cygznlem1  21556  chpdmatlem3  22815  txdis  23607  txdis1cn  23610  ptunhmeo  23783  qustgplem  24096  blcld  24480  nlmvscnlem2  24660  blcvx  24773  metds0  24826  metdseq0  24830  icopnfcnv  24919  lebnumii  24943  ipcau2  25211  tcphcphlem1  25212  ipcnlem2  25221  csbren  25376  trirn  25377  dyadf  25568  dyadovol  25570  dyaddisjlem  25572  dyadmaxlem  25574  opnmbllem  25578  mbfmulc2lem  25624  mbfi1fseqlem4  25695  mbfi1fseqlem5  25696  mbfi1fseqlem6  25697  itg2mulclem  25723  itg2monolem1  25727  itg2monolem3  25729  itg2cnlem2  25739  itgabs  25812  dvlip  25970  dvlt0  25982  dvcvx  25997  ftc1lem4  26016  dgrcolem2  26249  aaliou3lem2  26320  aaliou3lem9  26327  itgulm  26386  radcnvlem1  26391  abelthlem2  26410  abelthlem7  26416  tangtx  26482  cosne0  26506  cosordlem  26507  tanord1  26514  logdivlti  26597  logcnlem4  26622  logf1o2  26627  cxpcn3lem  26724  cxpaddle  26729  ang180lem2  26787  atanlogsublem  26892  atantan  26900  atanbndlem  26902  atans2  26908  leibpi  26919  log2tlbnd  26922  birthdaylem3  26930  efrlim  26946  efrlimOLD  26947  jensenlem2  26965  zetacvg  26992  ftalem1  27050  ftalem5  27054  basellem1  27058  basellem4  27061  fsumdvdsdiaglem  27160  dvdsflf1o  27164  fsumfldivdiaglem  27166  ppiub  27181  mersenne  27204  dchrptlem1  27241  bposlem1  27261  bposlem2  27262  bposlem4  27264  lgsdilem  27301  lgseisenlem1  27352  lgseisenlem2  27353  lgseisenlem3  27354  lgsquadlem1  27357  lgsquadlem2  27358  2sqlem3  27397  2sqlem8  27403  2sqlem11  27406  2sqblem  27408  chebbnd1lem2  27447  chebbnd1lem3  27448  rplogsumlem1  27461  rplogsumlem2  27462  dchrisumlem1  27466  dchrmusum2  27471  dchrisum0flblem1  27485  mulog2sumlem1  27511  logdivbnd  27533  pntpbnd1a  27562  pntpbnd1  27563  pntpbnd2  27564  pntlemh  27576  pntlemr  27579  pntlemk  27583  pntlemo  27584  ostth2lem1  27595  ostth2lem2  27611  ostth2lem3  27612  ostth3  27615  noextenddif  27646  noextendlt  27647  noextendgt  27648  nosupbnd1lem3  27688  nosupbnd1lem4  27689  nosupbnd1lem5  27690  nosupbnd1lem6  27691  noinfbnd1lem3  27703  noinfbnd1lem4  27704  noinfbnd1lem5  27705  noinfbnd1lem6  27706  noetasuplem4  27714  madecut  27889  cofcut2  27928  eucliddivs  28382  legov  28667  axsegcon  29010  axpaschlem  29023  0uhgrsubgr  29362  clwwlkf1  30134  upgr4cycl4dv4e  30270  eupth2lem3lem3  30315  nrt2irr  30558  nmblolbii  30885  nmbdoplbi  32110  nmcoplbi  32114  nmophmi  32117  nmbdfnlbi  32135  nmcfnlbi  32138  cnlnadjlem7  32159  nmopcoi  32181  resf1o  32818  receqid  32832  xdivrec  33001  cycpmfvlem  33188  cycpmfv3  33191  lbsdiflsp0  33786  txomap  33994  unitdivcld  34061  measvunilem  34372  measvuni  34374  measssd  34375  measiuns  34377  measinblem  34380  measdivcst  34384  sibfof  34500  oddpwdc  34514  sseqfv1  34549  sseqfv2  34554  probun  34579  totprobd  34586  dstrvprob  34632  actfunsnrndisj  34765  reprsuc  34775  breprexplema  34790  subfaclim  35386  connpconn  35433  cvmliftlem2  35484  cvmliftlem6  35488  cvmliftlem7  35489  cvmliftlem8  35490  cvmliftlem9  35491  cvmliftlem10  35492  snmlff  35527  lineext  36274  hilbert1.1  36352  nn0prpwlem  36520  poimirlem1  37956  opnmbllem0  37991  ismblfin  37996  itgabsnc  38024  ftc1cnnclem  38026  bfplem1  38157  bfp  38159  lfl1  39530  lfladdcl  39531  eqlkr  39559  lkrlsp  39562  atcvrj2b  39892  3dim1  39927  3dim2  39928  llni2  39972  2llnjaN  40026  lvoli3  40037  lvoli2  40041  lncvrelatN  40241  lhpat4N  40504  lhpat3  40506  4atexlemex6  40534  ldilco  40576  ltrnid  40595  ltrnatb  40597  ltrnel  40599  ltrncnvel  40602  ltrncnv  40606  ltrn11at  40607  ltrneq  40609  trlat  40629  trlator0  40631  ltrnnidn  40634  trlid0  40636  trlnidatb  40637  trlnle  40646  trlval3  40647  trlval4  40648  cdlemc2  40652  cdlemc5  40655  cdlemc6  40656  cdlemc  40657  cdlemd2  40659  cdlemd9  40666  cdleme0e  40677  cdleme02N  40682  cdleme0ex1N  40683  cdleme3e  40692  cdleme3g  40694  cdleme3h  40695  cdleme3  40697  cdleme7aa  40702  cdleme7b  40704  cdleme7c  40705  cdleme7d  40706  cdleme7e  40707  cdleme7ga  40708  cdleme7  40709  cdleme9  40713  cdleme16aN  40719  cdleme11c  40721  cdleme11dN  40722  cdleme11e  40723  cdleme11h  40726  cdleme11j  40727  cdleme11k  40728  cdleme12  40731  cdleme21j  40796  cdleme26eALTN  40821  cdleme26f  40823  cdleme26f2  40825  cdlemefrs29bpre0  40856  cdleme35a  40908  cdleme35b  40910  cdleme35c  40911  cdleme35f  40914  cdleme36a  40920  cdleme38m  40923  cdlemeg46rgv  40988  cdlemeg46req  40989  cdlemf  41023  cdlemg2fvlem  41054  cdlemg2l  41063  cdlemg7N  41086  cdlemg12g  41109  cdlemg15  41116  cdlemg17h  41128  cdlemg17  41137  cdlemg19a  41143  cdlemg24  41148  cdlemg37  41149  cdlemg27a  41152  cdlemg31b0N  41154  cdlemg27b  41156  cdlemg31c  41159  cdlemg31d  41160  cdlemg35  41173  trljco  41200  tgrpgrplem  41209  cdlemh2  41276  tendoconid  41289  tendotr  41290  cdlemk35s-id  41398  cdlemk39s-id  41400  cdlemk53b  41416  cdlemk53  41417  cdlemk54  41418  cdleml3N  41438  cdleml5N  41440  tendospcanN  41483  diclss  41653  dihvalcq2  41707  dihord4  41718  dihord5b  41719  dihord5apre  41722  dihmeetlem1N  41750  dihmeetbclemN  41764  dihmeetlem20N  41786  dihmeetALTN  41787  dihatlat  41794  dihatexv  41798  dochkr1  41938  dochkr1OLDN  41939  lcfl7lem  41959  lclkrlem2m  41979  hdmaplna1  42367  hdmaplns1  42368  hdmaplnm1  42369  cxp111d  42788  eldioph2lem1  43206  fphpdo  43263  irrapxlem1  43268  irrapxlem2  43269  irrapxlem3  43270  irrapxlem5  43272  pellexlem2  43276  pell1234qrreccl  43300  pell1234qrmulcl  43301  pell1234qrdich  43307  pell1qr1  43317  pellqrexplicit  43323  pellfundex  43332  reglogltb  43337  reglogleb  43338  pellfund14  43344  rmxycomplete  43363  jm2.24nn  43405  jm2.17b  43407  jm2.17c  43408  jm2.18  43434  jm2.19lem2  43436  jm2.20nn  43443  jm2.16nn0  43450  jm3.1lem2  43464  areaquad  43662  clsk3nimkb  44485  lemuldiv3d  44615  lemuldiv4d  44616  stoweidlem1  46447  stoweidlem11  46457  stoweidlem14  46460  stoweidlem26  46472  stoweidlem34  46480  stoweidlem38  46484  stoweidlem60  46506  fourierdlem52  46604  etransclem38  46718  2tceilhalfelfzo1  47796  reuopreuprim  47998  nprmdvdsfacm1lem4  48098  quad1  48108  requad1  48110  requad2  48111  isubgr3stgrlem1  48454  isubgr3stgrlem3  48456  gpg3kgrtriexlem1  48571  gpg3kgrtriexlem5  48575  domnmsuppn0  48857  lincvalpr  48906  ldepspr  48961  islindeps2  48971  fldivexpfllog2  49053  eenglngeehlnmlem1  49225  eenglngeehlnmlem2  49226  rrx2linest  49230  prsthinc  49951