Theorem syl112anc 1376

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 1088

This theorem is referenced by:  rmob2  3858  2nreu  4410  fveqf1o  7280  frrlem12  8279  enfixsn  9055  gruina  10778  grur1  10780  enqeq  10894  recrec  11886  rec11r  11888  divdivdiv  11890  dmdcan  11899  ddcan  11903  rereccl  11907  div2neg  11912  divmuld  11987  divmul2d  11998  divmul3d  11999  divassd  12000  div12d  12001  div23d  12002  divdird  12003  divsubdird  12004  div11d  12005  ltmul12a  12045  ltdiv1  12054  ltrec  12072  lt2msq1  12074  lediv2  12080  supmul1  12159  qbtwnre  13166  xlemul1a  13255  xlemul1  13257  xadd4d  13270  quoremz  13824  quoremnn0ALT  13826  expgt1  14072  nnlesq  14177  expnbnd  14204  expmulnbnd  14207  discr1  14211  facubnd  14272  pfxsuffeqwrdeq  14670  01sqrexlem6  15220  mulcn2  15569  geomulcvg  15849  cvgrat  15856  eftlub  16084  eflegeo  16096  tanhlt1  16135  sin01bnd  16160  cos01bnd  16161  eirrlem  16179  bitsmod  16413  mulgcd  16525  mulgcddvds  16632  prmind2  16662  qnumgt0  16727  pcpremul  16821  fldivp1  16875  pcfaclem  16876  qexpz  16879  prmpwdvds  16882  pockthg  16884  prmreclem1  16894  prmreclem5  16898  4sqlem10  16925  4sqlem12  16934  4sqlem16  16938  4sqlem17  16939  vdwlem3  16961  vdwlem8  16966  vdwlem9  16967  0ram  16998  ramz2  17002  cat1lem  18065  odmulg  19493  dfod2  19501  odf1o1  19509  odf1o2  19510  sylow3lem4  19567  ablsub4  19747  odadd1  19785  odadd2  19786  ablfacrp2  20006  ablfac1b  20009  ablfac1eu  20012  pgpfac1lem3a  20015  pgpfaclem2  20021  ablsimpgfindlem1  20046  chrcong  21444  znrrg  21482  cygznlem1  21483  chpdmatlem3  22734  txdis  23526  txdis1cn  23529  ptunhmeo  23702  qustgplem  24015  blcld  24400  nlmvscnlem2  24580  blcvx  24693  metds0  24746  metdseq0  24750  icopnfcnv  24847  lebnumii  24872  ipcau2  25141  tcphcphlem1  25142  ipcnlem2  25151  csbren  25306  trirn  25307  dyadf  25499  dyadovol  25501  dyaddisjlem  25503  dyadmaxlem  25505  opnmbllem  25509  mbfmulc2lem  25555  mbfi1fseqlem4  25626  mbfi1fseqlem5  25627  mbfi1fseqlem6  25628  itg2mulclem  25654  itg2monolem1  25658  itg2monolem3  25660  itg2cnlem2  25670  itgabs  25743  dvlip  25905  dvlt0  25917  dvcvx  25932  ftc1lem4  25953  dgrcolem2  26187  aaliou3lem2  26258  aaliou3lem9  26265  itgulm  26324  radcnvlem1  26329  abelthlem2  26349  abelthlem7  26355  tangtx  26421  cosne0  26445  cosordlem  26446  tanord1  26453  logdivlti  26536  logcnlem4  26561  logf1o2  26566  cxpcn3lem  26664  cxpaddle  26669  ang180lem2  26727  atanlogsublem  26832  atantan  26840  atanbndlem  26842  atans2  26848  leibpi  26859  log2tlbnd  26862  birthdaylem3  26870  efrlim  26886  efrlimOLD  26887  jensenlem2  26905  zetacvg  26932  ftalem1  26990  ftalem5  26994  basellem1  26998  basellem4  27001  fsumdvdsdiaglem  27100  dvdsflf1o  27104  fsumfldivdiaglem  27106  ppiub  27122  mersenne  27145  dchrptlem1  27182  bposlem1  27202  bposlem2  27203  bposlem4  27205  lgsdilem  27242  lgseisenlem1  27293  lgseisenlem2  27294  lgseisenlem3  27295  lgsquadlem1  27298  lgsquadlem2  27299  2sqlem3  27338  2sqlem8  27344  2sqlem11  27347  2sqblem  27349  chebbnd1lem2  27388  chebbnd1lem3  27389  rplogsumlem1  27402  rplogsumlem2  27403  dchrisumlem1  27407  dchrmusum2  27412  dchrisum0flblem1  27426  mulog2sumlem1  27452  logdivbnd  27474  pntpbnd1a  27503  pntpbnd1  27504  pntpbnd2  27505  pntlemh  27517  pntlemr  27520  pntlemk  27524  pntlemo  27525  ostth2lem1  27536  ostth2lem2  27552  ostth2lem3  27553  ostth3  27556  noextenddif  27587  noextendlt  27588  noextendgt  27589  nosupbnd1lem3  27629  nosupbnd1lem4  27630  nosupbnd1lem5  27631  nosupbnd1lem6  27632  noinfbnd1lem3  27644  noinfbnd1lem4  27645  noinfbnd1lem5  27646  noinfbnd1lem6  27647  noetasuplem4  27655  madecut  27801  cofcut2  27837  eucliddivs  28272  legov  28519  axsegcon  28861  axpaschlem  28874  0uhgrsubgr  29213  clwwlkf1  29985  upgr4cycl4dv4e  30121  eupth2lem3lem3  30166  nrt2irr  30409  nmblolbii  30735  nmbdoplbi  31960  nmcoplbi  31964  nmophmi  31967  nmbdfnlbi  31985  nmcfnlbi  31988  cnlnadjlem7  32009  nmopcoi  32031  resf1o  32660  muldivdid  32671  receqid  32675  xdivrec  32854  cycpmfvlem  33076  cycpmfv3  33079  lbsdiflsp0  33629  txomap  33831  unitdivcld  33898  measvunilem  34209  measvuni  34211  measssd  34212  measiuns  34214  measinblem  34217  measdivcst  34221  sibfof  34338  oddpwdc  34352  sseqfv1  34387  sseqfv2  34392  probun  34417  totprobd  34424  dstrvprob  34470  actfunsnrndisj  34603  reprsuc  34613  breprexplema  34628  subfaclim  35182  connpconn  35229  cvmliftlem2  35280  cvmliftlem6  35284  cvmliftlem7  35285  cvmliftlem8  35286  cvmliftlem9  35287  cvmliftlem10  35288  snmlff  35323  lineext  36071  hilbert1.1  36149  nn0prpwlem  36317  poimirlem1  37622  opnmbllem0  37657  ismblfin  37662  itgabsnc  37690  ftc1cnnclem  37692  bfplem1  37823  bfp  37825  lfl1  39070  lfladdcl  39071  eqlkr  39099  lkrlsp  39102  atcvrj2b  39433  3dim1  39468  3dim2  39469  llni2  39513  2llnjaN  39567  lvoli3  39578  lvoli2  39582  lncvrelatN  39782  lhpat4N  40045  lhpat3  40047  4atexlemex6  40075  ldilco  40117  ltrnid  40136  ltrnatb  40138  ltrnel  40140  ltrncnvel  40143  ltrncnv  40147  ltrn11at  40148  ltrneq  40150  trlat  40170  trlator0  40172  ltrnnidn  40175  trlid0  40177  trlnidatb  40178  trlnle  40187  trlval3  40188  trlval4  40189  cdlemc2  40193  cdlemc5  40196  cdlemc6  40197  cdlemc  40198  cdlemd2  40200  cdlemd9  40207  cdleme0e  40218  cdleme02N  40223  cdleme0ex1N  40224  cdleme3e  40233  cdleme3g  40235  cdleme3h  40236  cdleme3  40238  cdleme7aa  40243  cdleme7b  40245  cdleme7c  40246  cdleme7d  40247  cdleme7e  40248  cdleme7ga  40249  cdleme7  40250  cdleme9  40254  cdleme16aN  40260  cdleme11c  40262  cdleme11dN  40263  cdleme11e  40264  cdleme11h  40267  cdleme11j  40268  cdleme11k  40269  cdleme12  40272  cdleme21j  40337  cdleme26eALTN  40362  cdleme26f  40364  cdleme26f2  40366  cdlemefrs29bpre0  40397  cdleme35a  40449  cdleme35b  40451  cdleme35c  40452  cdleme35f  40455  cdleme36a  40461  cdleme38m  40464  cdlemeg46rgv  40529  cdlemeg46req  40530  cdlemf  40564  cdlemg2fvlem  40595  cdlemg2l  40604  cdlemg7N  40627  cdlemg12g  40650  cdlemg15  40657  cdlemg17h  40669  cdlemg17  40678  cdlemg19a  40684  cdlemg24  40689  cdlemg37  40690  cdlemg27a  40693  cdlemg31b0N  40695  cdlemg27b  40697  cdlemg31c  40700  cdlemg31d  40701  cdlemg35  40714  trljco  40741  tgrpgrplem  40750  cdlemh2  40817  tendoconid  40830  tendotr  40831  cdlemk35s-id  40939  cdlemk39s-id  40941  cdlemk53b  40957  cdlemk53  40958  cdlemk54  40959  cdleml3N  40979  cdleml5N  40981  tendospcanN  41024  diclss  41194  dihvalcq2  41248  dihord4  41259  dihord5b  41260  dihord5apre  41263  dihmeetlem1N  41291  dihmeetbclemN  41305  dihmeetlem20N  41327  dihmeetALTN  41328  dihatlat  41335  dihatexv  41339  dochkr1  41479  dochkr1OLDN  41480  lcfl7lem  41500  lclkrlem2m  41520  hdmaplna1  41908  hdmaplns1  41909  hdmaplnm1  41910  cxp111d  42337  eldioph2lem1  42755  fphpdo  42812  irrapxlem1  42817  irrapxlem2  42818  irrapxlem3  42819  irrapxlem5  42821  pellexlem2  42825  pell1234qrreccl  42849  pell1234qrmulcl  42850  pell1234qrdich  42856  pell1qr1  42866  pellqrexplicit  42872  pellfundex  42881  reglogltb  42886  reglogleb  42887  pellfund14  42893  rmxycomplete  42913  jm2.24nn  42955  jm2.17b  42957  jm2.17c  42958  jm2.18  42984  jm2.19lem2  42986  jm2.20nn  42993  jm2.16nn0  43000  jm3.1lem2  43014  areaquad  43212  clsk3nimkb  44036  lemuldiv3d  44166  lemuldiv4d  44167  stoweidlem1  46006  stoweidlem11  46016  stoweidlem14  46019  stoweidlem26  46031  stoweidlem34  46039  stoweidlem38  46043  stoweidlem60  46065  fourierdlem52  46163  etransclem38  46277  2tceilhalfelfzo1  47337  reuopreuprim  47531  quad1  47625  requad1  47627  requad2  47628  isubgr3stgrlem1  47969  isubgr3stgrlem3  47971  gpg3kgrtriexlem1  48078  gpg3kgrtriexlem5  48082  domnmsuppn0  48361  lincvalpr  48411  ldepspr  48466  islindeps2  48476  fldivexpfllog2  48558  eenglngeehlnmlem1  48730  eenglngeehlnmlem2  48731  rrx2linest  48735  prsthinc  49457