Theorem syl112anc 1397

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

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

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 1103

This theorem is referenced by:  rmob2  3848  2nreu  4401  fveqf1o  7290  frrlem12  8282  enfixsn  9062  gruina  10791  grur1  10793  enqeq  10907  muldivdid  11897  recrec  11900  rec11r  11902  divdivdiv  11904  dmdcan  11913  ddcan  11917  rereccl  11921  div2neg  11926  divmuld  12001  divmul2d  12012  divmul3d  12013  divassd  12014  div12d  12015  div23d  12016  divdird  12017  divsubdird  12018  div11d  12019  ltmul12a  12059  ltdiv1  12067  ltrec  12085  lt2msq1  12087  lediv2  12093  supmul1  12172  qbtwnre  13213  xlemul1a  13302  xlemul1  13304  xadd4d  13317  quoremz  13876  quoremnn0ALT  13878  expgt1  14124  nnlesq  14229  expnbnd  14256  expmulnbnd  14259  discr1  14263  facubnd  14324  pfxsuffeqwrdeq  14723  01sqrexlem6  15286  mulcn2  15635  geomulcvg  15918  cvgrat  15925  eftlub  16153  eflegeo  16165  tanhlt1  16204  sin01bnd  16229  cos01bnd  16230  eirrlem  16248  bitsmod  16482  mulgcd  16594  mulgcddvds  16701  prmind2  16731  qnumgt0  16797  pcpremul  16891  fldivp1  16945  pcfaclem  16946  qexpz  16949  prmpwdvds  16952  pockthg  16954  prmreclem1  16964  prmreclem5  16968  4sqlem10  16995  4sqlem12  17004  4sqlem16  17008  4sqlem17  17009  vdwlem3  17031  vdwlem8  17036  vdwlem9  17037  0ram  17068  ramz2  17072  cat1lem  18141  odmulg  19614  dfod2  19622  odf1o1  19630  odf1o2  19631  sylow3lem4  19688  ablsub4  19868  odadd1  19906  odadd2  19907  ablfacrp2  20127  ablfac1b  20130  ablfac1eu  20133  pgpfac1lem3a  20136  pgpfaclem2  20142  ablsimpgfindlem1  20167  chrcong  21634  znrrg  21672  cygznlem1  21673  chpdmatlem3  22954  txdis  23746  txdis1cn  23749  ptunhmeo  23922  qustgplem  24235  blcld  24619  nlmvscnlem2  24799  blcvx  24912  metds0  24965  metdseq0  24969  icopnfcnv  25058  lebnumii  25082  ipcau2  25350  tcphcphlem1  25351  ipcnlem2  25360  csbren  25515  trirn  25516  dyadf  25707  dyadovol  25709  dyaddisjlem  25711  dyadmaxlem  25713  opnmbllem  25717  mbfmulc2lem  25763  mbfi1fseqlem4  25834  mbfi1fseqlem5  25835  mbfi1fseqlem6  25836  itg2mulclem  25862  itg2monolem1  25866  itg2monolem3  25868  itg2cnlem2  25878  itgabs  25951  dvlip  26109  dvlt0  26121  dvcvx  26136  ftc1lem4  26155  dgrcolem2  26388  aaliou3lem2  26461  aaliou3lem9  26468  itgulm  26525  radcnvlem1  26530  abelthlem2  26549  abelthlem7  26555  tangtx  26624  cosne0  26648  cosordlem  26649  tanord1  26656  logdivlti  26739  logcnlem4  26764  logf1o2  26769  cxpcn3lem  26866  cxpaddle  26871  ang180lem2  26929  atanlogsublem  27034  atantan  27042  atanbndlem  27044  atans2  27050  leibpi  27061  log2tlbnd  27064  birthdaylem3  27072  efrlim  27088  jensenlem2  27106  zetacvg  27133  ftalem1  27191  ftalem5  27195  basellem1  27199  basellem4  27202  fsumdvdsdiaglem  27301  dvdsflf1o  27305  fsumfldivdiaglem  27307  ppiub  27322  mersenne  27345  dchrptlem1  27382  bposlem1  27402  bposlem2  27403  bposlem4  27405  lgsdilem  27442  lgseisenlem1  27493  lgseisenlem2  27494  lgseisenlem3  27495  lgsquadlem1  27498  lgsquadlem2  27499  2sqlem3  27538  2sqlem8  27544  2sqlem11  27547  2sqblem  27549  chebbnd1lem2  27588  chebbnd1lem3  27589  rplogsumlem1  27602  rplogsumlem2  27603  dchrisumlem1  27607  dchrmusum2  27612  dchrisum0flblem1  27626  mulog2sumlem1  27652  logdivbnd  27674  pntpbnd1a  27703  pntpbnd1  27704  pntpbnd2  27705  pntlemh  27717  pntlemr  27720  pntlemk  27724  pntlemo  27725  ostth2lem1  27736  ostth2lem2  27752  ostth2lem3  27753  ostth3  27756  noextenddif  27786  noextendlt  27787  noextendgt  27788  nosupbnd1lem3  27828  nosupbnd1lem4  27829  nosupbnd1lem5  27830  nosupbnd1lem6  27831  noinfbnd1lem3  27843  noinfbnd1lem4  27844  noinfbnd1lem5  27845  noinfbnd1lem6  27846  noetasuplem4  27854  madecut  28030  cofcut2  28069  eucliddivs  28523  legov  28808  axsegcon  29182  axpaschlem  29195  0uhgrsubgr  29534  clwwlkf1  30305  upgr4cycl4dv4e  30441  eupth2lem3lem3  30486  nrt2irr  30729  nmblolbii  31056  nmbdoplbi  32281  nmcoplbi  32285  nmophmi  32288  nmbdfnlbi  32306  nmcfnlbi  32309  cnlnadjlem7  32330  nmopcoi  32352  resf1o  32983  receqid  32997  xdivrec  33154  cycpmfvlem  33340  cycpmfv3  33343  lbsdiflsp0  33928  txomap  34136  unitdivcld  34203  measvunilem  34514  measvuni  34516  measssd  34517  measiuns  34519  measinblem  34522  measdivcst  34526  sibfof  34642  oddpwdc  34656  sseqfv1  34691  sseqfv2  34696  probun  34721  totprobd  34728  dstrvprob  34774  actfunsnrndisj  34904  reprsuc  34914  breprexplema  34929  subfaclim  35546  connpconn  35593  cvmliftlem2  35644  cvmliftlem6  35648  cvmliftlem7  35649  cvmliftlem8  35650  cvmliftlem9  35651  cvmliftlem10  35652  snmlff  35687  lineext  36434  hilbert1.1  36512  nn0prpwlem  36690  poimirlem1  38127  opnmbllem0  38162  ismblfin  38167  itgabsnc  38195  ftc1cnnclem  38197  bfplem1  38328  bfp  38330  lfl1  39701  lfladdcl  39702  eqlkr  39730  lkrlsp  39733  atcvrj2b  40063  3dim1  40098  3dim2  40099  llni2  40143  2llnjaN  40197  lvoli3  40208  lvoli2  40212  lncvrelatN  40412  lhpat4N  40675  lhpat3  40677  4atexlemex6  40705  ldilco  40747  ltrnid  40766  ltrnatb  40768  ltrnel  40770  ltrncnvel  40773  ltrncnv  40777  ltrn11at  40778  ltrneq  40780  trlat  40800  trlator0  40802  ltrnnidn  40805  trlid0  40807  trlnidatb  40808  trlnle  40817  trlval3  40818  trlval4  40819  cdlemc2  40823  cdlemc5  40826  cdlemc6  40827  cdlemc  40828  cdlemd2  40830  cdlemd9  40837  cdleme0e  40848  cdleme02N  40853  cdleme0ex1N  40854  cdleme3e  40863  cdleme3g  40865  cdleme3h  40866  cdleme3  40868  cdleme7aa  40873  cdleme7b  40875  cdleme7c  40876  cdleme7d  40877  cdleme7e  40878  cdleme7ga  40879  cdleme7  40880  cdleme9  40884  cdleme16aN  40890  cdleme11c  40892  cdleme11dN  40893  cdleme11e  40894  cdleme11h  40897  cdleme11j  40898  cdleme11k  40899  cdleme12  40902  cdleme21j  40967  cdleme26eALTN  40992  cdleme26f  40994  cdleme26f2  40996  cdlemefrs29bpre0  41027  cdleme35a  41079  cdleme35b  41081  cdleme35c  41082  cdleme35f  41085  cdleme36a  41091  cdleme38m  41094  cdlemeg46rgv  41159  cdlemeg46req  41160  cdlemf  41194  cdlemg2fvlem  41225  cdlemg2l  41234  cdlemg7N  41257  cdlemg12g  41280  cdlemg15  41287  cdlemg17h  41299  cdlemg17  41308  cdlemg19a  41314  cdlemg24  41319  cdlemg37  41320  cdlemg27a  41323  cdlemg31b0N  41325  cdlemg27b  41327  cdlemg31c  41330  cdlemg31d  41331  cdlemg35  41344  trljco  41371  tgrpgrplem  41380  cdlemh2  41447  tendoconid  41460  tendotr  41461  cdlemk35s-id  41569  cdlemk39s-id  41571  cdlemk53b  41587  cdlemk53  41588  cdlemk54  41589  cdleml3N  41609  cdleml5N  41611  tendospcanN  41654  diclss  41824  dihvalcq2  41878  dihord4  41889  dihord5b  41890  dihord5apre  41893  dihmeetlem1N  41921  dihmeetbclemN  41935  dihmeetlem20N  41957  dihmeetALTN  41958  dihatlat  41965  dihatexv  41969  dochkr1  42109  dochkr1OLDN  42110  lcfl7lem  42130  lclkrlem2m  42150  hdmaplna1  42538  hdmaplns1  42539  hdmaplnm1  42540  cxp111d  42958  eldioph2lem1  43348  fphpdo  43401  irrapxlem1  43406  irrapxlem2  43407  irrapxlem3  43408  irrapxlem5  43410  pellexlem2  43414  pell1234qrreccl  43438  pell1234qrmulcl  43439  pell1234qrdich  43445  pell1qr1  43455  pellqrexplicit  43461  pellfundex  43470  reglogltb  43475  reglogleb  43476  pellfund14  43482  rmxycomplete  43501  jm2.24nn  43543  jm2.17b  43545  jm2.17c  43546  jm2.18  43572  jm2.19lem2  43574  jm2.20nn  43581  jm2.16nn0  43588  jm3.1lem2  43602  areaquad  43800  clsk3nimkb  44623  lemuldiv3d  44753  lemuldiv4d  44754  stoweidlem1  46574  stoweidlem11  46584  stoweidlem14  46587  stoweidlem26  46599  stoweidlem34  46607  stoweidlem38  46611  stoweidlem60  46633  fourierdlem52  46731  etransclem38  46845  2tceilhalfelfzo1  47929  reuopreuprim  48131  nprmdvdsfacm1lem4  48231  quad1  48241  requad1  48243  requad2  48244  isubgr3stgrlem1  48587  isubgr3stgrlem3  48589  gpg3kgrtriexlem1  48704  gpg3kgrtriexlem5  48708  domnmsuppn0  49001  lincvalpr  49050  ldepspr  49105  islindeps2  49115  fldivexpfllog2  49197  eenglngeehlnmlem1  49369  eenglngeehlnmlem2  49370  rrx2linest  49374  prsthinc  50094