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 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  3892  2nreu  4444  fveqf1o  7322  frrlem12  8322  enfixsn  9121  gruina  10858  grur1  10860  enqeq  10974  recrec  11964  rec11r  11966  divdivdiv  11968  dmdcan  11977  ddcan  11981  rereccl  11985  div2neg  11990  divmuld  12065  divmul2d  12076  divmul3d  12077  divassd  12078  div12d  12079  div23d  12080  divdird  12081  divsubdird  12082  div11d  12083  ltmul12a  12123  ltdiv1  12132  ltrec  12150  lt2msq1  12152  lediv2  12158  supmul1  12237  qbtwnre  13241  xlemul1a  13330  xlemul1  13332  xadd4d  13345  quoremz  13895  quoremnn0ALT  13897  expgt1  14141  nnlesq  14244  expnbnd  14271  expmulnbnd  14274  discr1  14278  facubnd  14339  pfxsuffeqwrdeq  14736  01sqrexlem6  15286  mulcn2  15632  geomulcvg  15912  cvgrat  15919  eftlub  16145  eflegeo  16157  tanhlt1  16196  sin01bnd  16221  cos01bnd  16222  eirrlem  16240  bitsmod  16473  mulgcd  16585  mulgcddvds  16692  prmind2  16722  qnumgt0  16787  pcpremul  16881  fldivp1  16935  pcfaclem  16936  qexpz  16939  prmpwdvds  16942  pockthg  16944  prmreclem1  16954  prmreclem5  16958  4sqlem10  16985  4sqlem12  16994  4sqlem16  16998  4sqlem17  16999  vdwlem3  17021  vdwlem8  17026  vdwlem9  17027  0ram  17058  ramz2  17062  cat1lem  18141  odmulg  19574  dfod2  19582  odf1o1  19590  odf1o2  19591  sylow3lem4  19648  ablsub4  19828  odadd1  19866  odadd2  19867  ablfacrp2  20087  ablfac1b  20090  ablfac1eu  20093  pgpfac1lem3a  20096  pgpfaclem2  20102  ablsimpgfindlem1  20127  chrcong  21542  znrrg  21584  cygznlem1  21585  chpdmatlem3  22846  txdis  23640  txdis1cn  23643  ptunhmeo  23816  qustgplem  24129  blcld  24518  nlmvscnlem2  24706  blcvx  24819  metds0  24872  metdseq0  24876  icopnfcnv  24973  lebnumii  24998  ipcau2  25268  tcphcphlem1  25269  ipcnlem2  25278  csbren  25433  trirn  25434  dyadf  25626  dyadovol  25628  dyaddisjlem  25630  dyadmaxlem  25632  opnmbllem  25636  mbfmulc2lem  25682  mbfi1fseqlem4  25753  mbfi1fseqlem5  25754  mbfi1fseqlem6  25755  itg2mulclem  25781  itg2monolem1  25785  itg2monolem3  25787  itg2cnlem2  25797  itgabs  25870  dvlip  26032  dvlt0  26044  dvcvx  26059  ftc1lem4  26080  dgrcolem2  26314  aaliou3lem2  26385  aaliou3lem9  26392  itgulm  26451  radcnvlem1  26456  abelthlem2  26476  abelthlem7  26482  tangtx  26547  cosne0  26571  cosordlem  26572  tanord1  26579  logdivlti  26662  logcnlem4  26687  logf1o2  26692  cxpcn3lem  26790  cxpaddle  26795  ang180lem2  26853  atanlogsublem  26958  atantan  26966  atanbndlem  26968  atans2  26974  leibpi  26985  log2tlbnd  26988  birthdaylem3  26996  efrlim  27012  efrlimOLD  27013  jensenlem2  27031  zetacvg  27058  ftalem1  27116  ftalem5  27120  basellem1  27124  basellem4  27127  fsumdvdsdiaglem  27226  dvdsflf1o  27230  fsumfldivdiaglem  27232  ppiub  27248  mersenne  27271  dchrptlem1  27308  bposlem1  27328  bposlem2  27329  bposlem4  27331  lgsdilem  27368  lgseisenlem1  27419  lgseisenlem2  27420  lgseisenlem3  27421  lgsquadlem1  27424  lgsquadlem2  27425  2sqlem3  27464  2sqlem8  27470  2sqlem11  27473  2sqblem  27475  chebbnd1lem2  27514  chebbnd1lem3  27515  rplogsumlem1  27528  rplogsumlem2  27529  dchrisumlem1  27533  dchrmusum2  27538  dchrisum0flblem1  27552  mulog2sumlem1  27578  logdivbnd  27600  pntpbnd1a  27629  pntpbnd1  27630  pntpbnd2  27631  pntlemh  27643  pntlemr  27646  pntlemk  27650  pntlemo  27651  ostth2lem1  27662  ostth2lem2  27678  ostth2lem3  27679  ostth3  27682  noextenddif  27713  noextendlt  27714  noextendgt  27715  nosupbnd1lem3  27755  nosupbnd1lem4  27756  nosupbnd1lem5  27757  nosupbnd1lem6  27758  noinfbnd1lem3  27770  noinfbnd1lem4  27771  noinfbnd1lem5  27772  noinfbnd1lem6  27773  noetasuplem4  27781  madecut  27921  cofcut2  27956  legov  28593  axsegcon  28942  axpaschlem  28955  0uhgrsubgr  29296  clwwlkf1  30068  upgr4cycl4dv4e  30204  eupth2lem3lem3  30249  nrt2irr  30492  nmblolbii  30818  nmbdoplbi  32043  nmcoplbi  32047  nmophmi  32050  nmbdfnlbi  32068  nmcfnlbi  32071  cnlnadjlem7  32092  nmopcoi  32114  resf1o  32741  muldivdid  32751  xdivrec  32909  cycpmfvlem  33132  cycpmfv3  33135  lbsdiflsp0  33677  txomap  33833  unitdivcld  33900  measvunilem  34213  measvuni  34215  measssd  34216  measiuns  34218  measinblem  34221  measdivcst  34225  sibfof  34342  oddpwdc  34356  sseqfv1  34391  sseqfv2  34396  probun  34421  totprobd  34428  dstrvprob  34474  actfunsnrndisj  34620  reprsuc  34630  breprexplema  34645  subfaclim  35193  connpconn  35240  cvmliftlem2  35291  cvmliftlem6  35295  cvmliftlem7  35296  cvmliftlem8  35297  cvmliftlem9  35298  cvmliftlem10  35299  snmlff  35334  lineext  36077  hilbert1.1  36155  nn0prpwlem  36323  poimirlem1  37628  opnmbllem0  37663  ismblfin  37668  itgabsnc  37696  ftc1cnnclem  37698  bfplem1  37829  bfp  37831  lfl1  39071  lfladdcl  39072  eqlkr  39100  lkrlsp  39103  atcvrj2b  39434  3dim1  39469  3dim2  39470  llni2  39514  2llnjaN  39568  lvoli3  39579  lvoli2  39583  lncvrelatN  39783  lhpat4N  40046  lhpat3  40048  4atexlemex6  40076  ldilco  40118  ltrnid  40137  ltrnatb  40139  ltrnel  40141  ltrncnvel  40144  ltrncnv  40148  ltrn11at  40149  ltrneq  40151  trlat  40171  trlator0  40173  ltrnnidn  40176  trlid0  40178  trlnidatb  40179  trlnle  40188  trlval3  40189  trlval4  40190  cdlemc2  40194  cdlemc5  40197  cdlemc6  40198  cdlemc  40199  cdlemd2  40201  cdlemd9  40208  cdleme0e  40219  cdleme02N  40224  cdleme0ex1N  40225  cdleme3e  40234  cdleme3g  40236  cdleme3h  40237  cdleme3  40239  cdleme7aa  40244  cdleme7b  40246  cdleme7c  40247  cdleme7d  40248  cdleme7e  40249  cdleme7ga  40250  cdleme7  40251  cdleme9  40255  cdleme16aN  40261  cdleme11c  40263  cdleme11dN  40264  cdleme11e  40265  cdleme11h  40268  cdleme11j  40269  cdleme11k  40270  cdleme12  40273  cdleme21j  40338  cdleme26eALTN  40363  cdleme26f  40365  cdleme26f2  40367  cdlemefrs29bpre0  40398  cdleme35a  40450  cdleme35b  40452  cdleme35c  40453  cdleme35f  40456  cdleme36a  40462  cdleme38m  40465  cdlemeg46rgv  40530  cdlemeg46req  40531  cdlemf  40565  cdlemg2fvlem  40596  cdlemg2l  40605  cdlemg7N  40628  cdlemg12g  40651  cdlemg15  40658  cdlemg17h  40670  cdlemg17  40679  cdlemg19a  40685  cdlemg24  40690  cdlemg37  40691  cdlemg27a  40694  cdlemg31b0N  40696  cdlemg27b  40698  cdlemg31c  40701  cdlemg31d  40702  cdlemg35  40715  trljco  40742  tgrpgrplem  40751  cdlemh2  40818  tendoconid  40831  tendotr  40832  cdlemk35s-id  40940  cdlemk39s-id  40942  cdlemk53b  40958  cdlemk53  40959  cdlemk54  40960  cdleml3N  40980  cdleml5N  40982  tendospcanN  41025  diclss  41195  dihvalcq2  41249  dihord4  41260  dihord5b  41261  dihord5apre  41264  dihmeetlem1N  41292  dihmeetbclemN  41306  dihmeetlem20N  41328  dihmeetALTN  41329  dihatlat  41336  dihatexv  41340  dochkr1  41480  dochkr1OLDN  41481  lcfl7lem  41501  lclkrlem2m  41521  hdmaplna1  41909  hdmaplns1  41910  hdmaplnm1  41911  cxp111d  42378  eldioph2lem1  42771  fphpdo  42828  irrapxlem1  42833  irrapxlem2  42834  irrapxlem3  42835  irrapxlem5  42837  pellexlem2  42841  pell1234qrreccl  42865  pell1234qrmulcl  42866  pell1234qrdich  42872  pell1qr1  42882  pellqrexplicit  42888  pellfundex  42897  reglogltb  42902  reglogleb  42903  pellfund14  42909  rmxycomplete  42929  jm2.24nn  42971  jm2.17b  42973  jm2.17c  42974  jm2.18  43000  jm2.19lem2  43002  jm2.20nn  43009  jm2.16nn0  43016  jm3.1lem2  43030  areaquad  43228  clsk3nimkb  44053  lemuldiv3d  44183  lemuldiv4d  44184  stoweidlem1  46016  stoweidlem11  46026  stoweidlem14  46029  stoweidlem26  46041  stoweidlem34  46049  stoweidlem38  46053  stoweidlem60  46075  fourierdlem52  46173  etransclem38  46287  reuopreuprim  47513  quad1  47607  requad1  47609  requad2  47610  isubgr3stgrlem1  47933  isubgr3stgrlem3  47935  2tceilhalfelfzo1  48018  gpg3kgrtriexlem1  48039  gpg3kgrtriexlem5  48043  domnmsuppn0  48285  lincvalpr  48335  ldepspr  48390  islindeps2  48400  fldivexpfllog2  48486  eenglngeehlnmlem1  48658  eenglngeehlnmlem2  48659  rrx2linest  48663  prsthinc  49111