Theorem syl112anc 1401

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  rmob2  3847  2nreu  4410  fveqf1o  7302  frrlem12  8295  enfixsn  9075  gruina  10804  grur1  10806  enqeq  10920  muldivdid  11910  recrec  11913  rec11r  11915  divdivdiv  11917  dmdcan  11926  ddcan  11930  rereccl  11934  div2neg  11939  divmuld  12014  divmul2d  12025  divmul3d  12026  divassd  12027  div12d  12028  div23d  12029  divdird  12030  divsubdird  12031  div11d  12032  ltmul12a  12072  ltdiv1  12080  ltrec  12098  lt2msq1  12100  lediv2  12106  supmul1  12185  qbtwnre  13226  xlemul1a  13315  xlemul1  13317  xadd4d  13330  quoremz  13890  quoremnn0ALT  13892  expgt1  14138  nnlesq  14243  expnbnd  14270  expmulnbnd  14273  discr1  14277  facubnd  14338  pfxsuffeqwrdeq  14737  01sqrexlem6  15300  mulcn2  15649  geomulcvg  15932  cvgrat  15939  eftlub  16166  eflegeo  16178  tanhlt1  16217  sin01bnd  16242  cos01bnd  16243  eirrlem  16261  bitsmod  16495  mulgcd  16607  mulgcddvds  16714  prmind2  16744  qnumgt0  16810  pcpremul  16904  fldivp1  16958  pcfaclem  16959  qexpz  16962  prmpwdvds  16965  pockthg  16967  prmreclem1  16977  prmreclem5  16981  4sqlem10  17008  4sqlem12  17017  4sqlem16  17021  4sqlem17  17022  vdwlem3  17044  vdwlem8  17049  vdwlem9  17050  0ram  17081  ramz2  17085  cat1lem  18154  odmulg  19627  dfod2  19635  odf1o1  19643  odf1o2  19644  sylow3lem4  19701  ablsub4  19881  odadd1  19919  odadd2  19920  ablfacrp2  20140  ablfac1b  20143  ablfac1eu  20146  pgpfac1lem3a  20149  pgpfaclem2  20155  ablsimpgfindlem1  20180  chrcong  21658  znrrg  21696  cygznlem1  21697  chpdmatlem3  22978  txdis  23770  txdis1cn  23773  ptunhmeo  23946  qustgplem  24259  blcld  24643  nlmvscnlem2  24823  blcvx  24936  metds0  24989  metdseq0  24993  icopnfcnv  25082  lebnumii  25106  ipcau2  25374  tcphcphlem1  25375  ipcnlem2  25384  csbren  25539  trirn  25540  dyadf  25731  dyadovol  25733  dyaddisjlem  25735  dyadmaxlem  25737  opnmbllem  25741  mbfmulc2lem  25787  mbfi1fseqlem4  25858  mbfi1fseqlem5  25859  mbfi1fseqlem6  25860  itg2mulclem  25886  itg2monolem1  25890  itg2monolem3  25892  itg2cnlem2  25902  itgabs  25975  dvlip  26133  dvlt0  26145  dvcvx  26160  ftc1lem4  26179  dgrcolem2  26412  aaliou3lem2  26487  aaliou3lem9  26494  itgulm  26552  radcnvlem1  26557  abelthlem2  26576  abelthlem7  26582  tangtx  26651  cosne0  26675  cosordlem  26676  tanord1  26683  logdivlti  26766  logcnlem4  26791  logf1o2  26796  cxpcn3lem  26893  cxpaddle  26898  ang180lem2  26956  atanlogsublem  27061  atantan  27069  atanbndlem  27071  atans2  27077  leibpi  27088  log2tlbnd  27091  birthdaylem3  27099  efrlim  27115  jensenlem2  27133  zetacvg  27160  ftalem1  27218  ftalem5  27222  basellem1  27226  basellem4  27229  fsumdvdsdiaglem  27328  dvdsflf1o  27332  fsumfldivdiaglem  27334  ppiub  27349  mersenne  27372  dchrptlem1  27409  bposlem1  27429  bposlem2  27430  bposlem4  27432  lgsdilem  27469  lgseisenlem1  27520  lgseisenlem2  27521  lgseisenlem3  27522  lgsquadlem1  27525  lgsquadlem2  27526  2sqlem3  27565  2sqlem8  27571  2sqlem11  27574  2sqblem  27576  chebbnd1lem2  27615  chebbnd1lem3  27616  rplogsumlem1  27629  rplogsumlem2  27630  dchrisumlem1  27634  dchrmusum2  27639  dchrisum0flblem1  27653  mulog2sumlem1  27679  logdivbnd  27701  pntpbnd1a  27730  pntpbnd1  27731  pntpbnd2  27732  pntlemh  27744  pntlemr  27747  pntlemk  27751  pntlemo  27752  ostth2lem1  27763  ostth2lem2  27779  ostth2lem3  27780  ostth3  27783  noextenddif  27813  noextendlt  27814  noextendgt  27815  nosupbnd1lem3  27855  nosupbnd1lem4  27856  nosupbnd1lem5  27857  nosupbnd1lem6  27858  noinfbnd1lem3  27870  noinfbnd1lem4  27871  noinfbnd1lem5  27872  noinfbnd1lem6  27873  noetasuplem4  27881  madecut  28057  cofcut2  28096  eucliddivs  28550  legov  28835  axsegcon  29258  axpaschlem  29271  0uhgrsubgr  29610  clwwlkf1  30381  upgr4cycl4dv4e  30517  eupth2lem3lem3  30562  nrt2irr  30805  nmblolbii  31132  nmbdoplbi  32357  nmcoplbi  32361  nmophmi  32364  nmbdfnlbi  32382  nmcfnlbi  32385  cnlnadjlem7  32406  nmopcoi  32428  resf1o  33056  receqid  33070  xdivrec  33227  cycpmfvlem  33413  cycpmfv3  33416  lbsdiflsp0  33997  txomap  34205  unitdivcld  34272  measvunilem  34583  measvuni  34585  measssd  34586  measiuns  34588  measinblem  34591  measdivcst  34595  sibfof  34711  oddpwdc  34725  sseqfv1  34760  sseqfv2  34765  probun  34790  totprobd  34797  dstrvprob  34843  actfunsnrndisj  34973  reprsuc  34983  breprexplema  34998  subfaclim  35661  connpconn  35708  cvmliftlem2  35759  cvmliftlem6  35763  cvmliftlem7  35764  cvmliftlem8  35765  cvmliftlem9  35766  cvmliftlem10  35767  snmlff  35802  lineext  36549  hilbert1.1  36627  nn0prpwlem  36814  poimirlem1  38253  opnmbllem0  38288  ismblfin  38293  itgabsnc  38321  ftc1cnnclem  38323  bfplem1  38454  bfp  38456  lfl1  39825  lfladdcl  39826  eqlkr  39854  lkrlsp  39857  atcvrj2b  40187  3dim1  40222  3dim2  40223  llni2  40267  2llnjaN  40321  lvoli3  40332  lvoli2  40336  lncvrelatN  40536  lhpat4N  40799  lhpat3  40801  4atexlemex6  40829  ldilco  40871  ltrnid  40890  ltrnatb  40892  ltrnel  40894  ltrncnvel  40897  ltrncnv  40901  ltrn11at  40902  ltrneq  40904  trlat  40924  trlator0  40926  ltrnnidn  40929  trlid0  40931  trlnidatb  40932  trlnle  40941  trlval3  40942  trlval4  40943  cdlemc2  40947  cdlemc5  40950  cdlemc6  40951  cdlemc  40952  cdlemd2  40954  cdlemd9  40961  cdleme0e  40972  cdleme02N  40977  cdleme0ex1N  40978  cdleme3e  40987  cdleme3g  40989  cdleme3h  40990  cdleme3  40992  cdleme7aa  40997  cdleme7b  40999  cdleme7c  41000  cdleme7d  41001  cdleme7e  41002  cdleme7ga  41003  cdleme7  41004  cdleme9  41008  cdleme16aN  41014  cdleme11c  41016  cdleme11dN  41017  cdleme11e  41018  cdleme11h  41021  cdleme11j  41022  cdleme11k  41023  cdleme12  41026  cdleme21j  41091  cdleme26eALTN  41116  cdleme26f  41118  cdleme26f2  41120  cdlemefrs29bpre0  41151  cdleme35a  41203  cdleme35b  41205  cdleme35c  41206  cdleme35f  41209  cdleme36a  41215  cdleme38m  41218  cdlemeg46rgv  41283  cdlemeg46req  41284  cdlemf  41318  cdlemg2fvlem  41349  cdlemg2l  41358  cdlemg7N  41381  cdlemg12g  41404  cdlemg15  41411  cdlemg17h  41423  cdlemg17  41432  cdlemg19a  41438  cdlemg24  41443  cdlemg37  41444  cdlemg27a  41447  cdlemg31b0N  41449  cdlemg27b  41451  cdlemg31c  41454  cdlemg31d  41455  cdlemg35  41468  trljco  41495  tgrpgrplem  41504  cdlemh2  41571  tendoconid  41584  tendotr  41585  cdlemk35s-id  41693  cdlemk39s-id  41695  cdlemk53b  41711  cdlemk53  41712  cdlemk54  41713  cdleml3N  41733  cdleml5N  41735  tendospcanN  41778  diclss  41948  dihvalcq2  42002  dihord4  42013  dihord5b  42014  dihord5apre  42017  dihmeetlem1N  42045  dihmeetbclemN  42059  dihmeetlem20N  42081  dihmeetALTN  42082  dihatlat  42089  dihatexv  42093  dochkr1  42233  dochkr1OLDN  42234  lcfl7lem  42254  lclkrlem2m  42274  hdmaplna1  42662  hdmaplns1  42663  hdmaplnm1  42664  cxp111d  43084  eldioph2lem1  43474  fphpdo  43527  irrapxlem1  43532  irrapxlem2  43533  irrapxlem3  43534  irrapxlem5  43536  pellexlem2  43540  pell1234qrreccl  43564  pell1234qrmulcl  43565  pell1234qrdich  43571  pell1qr1  43581  pellqrexplicit  43587  pellfundex  43596  reglogltb  43601  reglogleb  43602  pellfund14  43608  rmxycomplete  43627  jm2.24nn  43669  jm2.17b  43671  jm2.17c  43672  jm2.18  43698  jm2.19lem2  43700  jm2.20nn  43707  jm2.16nn0  43714  jm3.1lem2  43728  areaquad  43926  clsk3nimkb  44749  lemuldiv3d  44879  lemuldiv4d  44880  stoweidlem1  46698  stoweidlem11  46708  stoweidlem14  46711  stoweidlem26  46723  stoweidlem34  46731  stoweidlem38  46735  stoweidlem60  46757  fourierdlem52  46855  etransclem38  46969  2tceilhalfelfzo1  48056  reuopreuprim  48258  nprmdvdsfacm1lem4  48358  quad1  48368  requad1  48370  requad2  48371  isubgr3stgrlem1  48714  isubgr3stgrlem3  48716  gpg3kgrtriexlem1  48831  gpg3kgrtriexlem5  48835  domnmsuppn0  49132  lincvalpr  49181  ldepspr  49236  islindeps2  49246  fldivexpfllog2  49328  eenglngeehlnmlem1  49500  eenglngeehlnmlem2  49501  rrx2linest  49505  prsthinc  50225