Theorem syl112anc 1322

Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)

Hypotheses

Ref	Expression
syl12anc.1	⊢ (𝜑 → 𝜓)
syl12anc.2	⊢ (𝜑 → 𝜒)
syl12anc.3	⊢ (𝜑 → 𝜃)
syl22anc.4	⊢ (𝜑 → 𝜏)
syl112anc.5	⊢ ((𝜓 ∧ 𝜒 ∧ (𝜃 ∧ 𝜏)) → 𝜂)

Assertion

Ref	Expression
syl112anc	⊢ (𝜑 → 𝜂)

Proof of Theorem syl112anc

Step	Hyp	Ref	Expression
1		syl12anc.1	. 2 ⊢ (𝜑 → 𝜓)
2		syl12anc.2	. 2 ⊢ (𝜑 → 𝜒)
3		syl12anc.3	. . 3 ⊢ (𝜑 → 𝜃)
4		syl22anc.4	. . 3 ⊢ (𝜑 → 𝜏)
5	3, 4	jca 553	. 2 ⊢ (𝜑 → (𝜃 ∧ 𝜏))
6		syl112anc.5	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ (𝜃 ∧ 𝜏)) → 𝜂)
7	1, 2, 5, 6	syl3anc 1318	1 ⊢ (𝜑 → 𝜂)

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  rmob2  3497  fveqf1o  6457  enfixsn  7954  gruina  9519  grur1  9521  enqeq  9635  recrec  10601  rec11r  10603  divdivdiv  10605  dmdcan  10614  ddcan  10618  rereccl  10622  div2neg  10627  divmuld  10702  divmul2d  10713  divmul3d  10714  divassd  10715  div12d  10716  div23d  10717  divdird  10718  divsubdird  10719  div11d  10720  ltmul12a  10758  ltdiv1  10766  ltrec  10784  lt2msq1  10786  lediv2  10792  supmul1  10869  qbtwnre  11904  xlemul1a  11990  xlemul1  11992  xadd4d  12005  quoremz  12516  quoremnn0ALT  12518  expgt1  12760  nnlesq  12830  expnbnd  12855  expmulnbnd  12858  discr1  12862  facubnd  12949  hashf1lem1  13096  2swrdeqwrdeq  13305  sqrlem6  13836  mulcn2  14174  climcnds  14422  geomulcvg  14446  cvgrat  14454  eftlub  14678  eflegeo  14690  tanhlt1  14729  sin01bnd  14754  cos01bnd  14755  eirrlem  14771  bitsmod  14996  mulgcd  15103  mulgcddvds  15207  prmind2  15236  qnumgt0  15296  iserodd  15378  pcpremul  15386  fldivp1  15439  pcfaclem  15440  qexpz  15443  prmpwdvds  15446  pockthg  15448  prmreclem1  15458  prmreclem5  15462  4sqlem10  15489  4sqlem12  15498  4sqlem16  15502  4sqlem17  15503  vdwlem3  15525  vdwlem8  15530  vdwlem9  15531  0ram  15562  ramz2  15566  xpsc0  16043  xpsc1  16044  odmulg  17796  dfod2  17804  odf1o1  17810  odf1o2  17811  sylow3lem4  17868  ablsub4  18041  odadd1  18074  odadd2  18075  ablfacrp2  18289  ablfac1b  18292  ablfac1eu  18295  pgpfac1lem3a  18298  pgpfaclem2  18304  chrcong  19696  znrrg  19733  cygznlem1  19734  chpdmatlem3  20464  txdis  21245  txdis1cn  21248  ptunhmeo  21421  qustgplem  21734  blcld  22120  nlmvscnlem2  22299  blcvx  22409  metds0  22461  metdseq0  22465  icopnfcnv  22549  lebnumii  22573  ipcau2  22841  tchcphlem1  22842  ipcnlem2  22851  csbren  22990  trirn  22991  dyadf  23165  dyadovol  23167  dyaddisjlem  23169  dyadmaxlem  23171  opnmbllem  23175  mbfmulc2lem  23220  mbfi1fseqlem4  23291  mbfi1fseqlem5  23292  mbfi1fseqlem6  23293  itg2mulclem  23319  itg2monolem1  23323  itg2monolem3  23325  itg2cnlem2  23335  itgabs  23407  dvlip  23560  dvlt0  23572  dvcvx  23587  ftc1lem4  23606  dgrcolem2  23834  aaliou3lem2  23902  aaliou3lem9  23909  itgulm  23966  radcnvlem1  23971  abelthlem2  23990  abelthlem7  23996  tangtx  24061  cosne0  24080  cosordlem  24081  tanord1  24087  logdivlti  24170  logcnlem4  24191  logf1o2  24196  cxpcn3lem  24288  cxpaddle  24293  ang180lem2  24340  atanlogsublem  24442  atantan  24450  atanbndlem  24452  atans2  24458  leibpi  24469  log2tlbnd  24472  birthdaylem3  24480  efrlim  24496  jensenlem2  24514  zetacvg  24541  ftalem1  24599  ftalem5  24603  basellem1  24607  basellem4  24610  fsumdvdsdiaglem  24709  dvdsflf1o  24713  fsumfldivdiaglem  24715  ppiub  24729  mersenne  24752  dchrptlem1  24789  bposlem1  24809  bposlem2  24810  bposlem4  24812  lgsdilem  24849  lgseisenlem1  24900  lgseisenlem2  24901  lgseisenlem3  24902  lgsquadlem1  24905  lgsquadlem2  24906  2sqlem3  24945  2sqlem8  24951  2sqlem11  24954  2sqblem  24956  chebbnd1lem2  24959  chebbnd1lem3  24960  rplogsumlem1  24973  rplogsumlem2  24974  dchrisumlem1  24978  dchrmusum2  24983  dchrisum0flblem1  24997  mulog2sumlem1  25023  logdivbnd  25045  pntpbnd1a  25074  pntpbnd1  25075  pntpbnd2  25076  pntlemh  25088  pntlemr  25091  pntlemk  25095  pntlemo  25096  ostth2lem1  25107  ostth2lem2  25123  ostth2lem3  25124  ostth3  25127  legov  25280  axsegcon  25607  axpaschlem  25620  clwwlkf1  26324  vdgrun  26428  vdgrfiun  26429  eupath2lem3  26506  nmblolbii  27038  nmbdoplbi  28267  nmcoplbi  28271  nmophmi  28274  nmbdfnlbi  28292  nmcfnlbi  28295  cnlnadjlem7  28316  nmopcoi  28338  resf1o  28893  xdivrec  28966  txomap  29229  unitdivcld  29275  measvunilem  29602  measvuni  29604  measssd  29605  measiuns  29607  measinblem  29610  measdivcst  29615  sibfof  29729  oddpwdc  29743  sseqfv1  29778  sseqfv2  29783  probun  29808  totprobd  29815  dstrvprob  29860  subfaclim  30424  conpcon  30471  cvmliftlem2  30522  cvmliftlem6  30526  cvmliftlem7  30527  cvmliftlem8  30528  cvmliftlem9  30529  cvmliftlem10  30530  snmlff  30565  lineext  31353  hilbert1.1  31431  nn0prpwlem  31487  poimirlem1  32580  opnmbllem0  32615  ismblfin  32620  itgabsnc  32649  ftc1cnnclem  32653  bfplem1  32791  bfp  32793  lfl1  33375  lfladdcl  33376  eqlkr  33404  lkrlsp  33407  atcvrj2b  33736  3dim1  33771  3dim2  33772  llni2  33816  2llnjaN  33870  lvoli3  33881  lvoli2  33885  lncvrelatN  34085  lhpat4N  34348  lhpat3  34350  4atexlemex6  34378  ldilco  34420  ltrnid  34439  ltrnatb  34441  ltrnel  34443  ltrncnvel  34446  ltrncnv  34450  ltrn11at  34451  ltrneq  34453  ltrnmwOLD  34456  trlat  34474  trlator0  34476  ltrnnidn  34479  trlid0  34481  trlnidatb  34482  trlnle  34491  trlval3  34492  trlval4  34493  cdlemc2  34497  cdlemc5  34500  cdlemc6  34501  cdlemc  34502  cdlemd2  34504  cdlemd9  34511  cdleme0e  34522  cdleme02N  34527  cdleme0ex1N  34528  cdleme3e  34537  cdleme3g  34539  cdleme3h  34540  cdleme3  34542  cdleme7aa  34547  cdleme7b  34549  cdleme7c  34550  cdleme7d  34551  cdleme7e  34552  cdleme7ga  34553  cdleme7  34554  cdleme9  34558  cdleme16aN  34564  cdleme11c  34566  cdleme11dN  34567  cdleme11e  34568  cdleme11h  34571  cdleme11j  34572  cdleme11k  34573  cdleme12  34576  cdleme21j  34642  cdleme26eALTN  34667  cdleme26f  34669  cdleme26f2  34671  cdlemefrs29bpre0  34702  cdleme35a  34754  cdleme35b  34756  cdleme35c  34757  cdleme35f  34760  cdleme36a  34766  cdleme38m  34769  cdlemeg46rgv  34834  cdlemeg46req  34835  cdlemf  34869  cdlemg2fvlem  34900  cdlemg2l  34909  cdlemg7N  34932  cdlemg12g  34955  cdlemg15  34962  cdlemg17h  34974  cdlemg17  34983  cdlemg19a  34989  cdlemg24  34994  cdlemg37  34995  cdlemg27a  34998  cdlemg31b0N  35000  cdlemg27b  35002  cdlemg31c  35005  cdlemg31d  35006  cdlemg35  35019  trljco  35046  tgrpgrplem  35055  cdlemh2  35122  tendoconid  35135  tendotr  35136  cdlemk35s-id  35244  cdlemk39s-id  35246  cdlemk53b  35262  cdlemk53  35263  cdlemk54  35264  cdleml3N  35284  cdleml5N  35286  tendospcanN  35330  diclss  35500  dihvalcq2  35554  dihord4  35565  dihord5b  35566  dihord5apre  35569  dihmeetlem1N  35597  dihmeetbclemN  35611  dihmeetlem20N  35633  dihmeetALTN  35634  dihatlat  35641  dihatexv  35645  dochkr1  35785  dochkr1OLDN  35786  lcfl7lem  35806  lclkrlem2m  35826  hdmaplna1  36217  hdmaplns1  36218  hdmaplnm1  36219  eldioph2lem1  36341  fphpdo  36399  irrapxlem1  36404  irrapxlem2  36405  irrapxlem3  36406  irrapxlem5  36408  pellexlem2  36412  pell1234qrreccl  36436  pell1234qrmulcl  36437  pell1234qrdich  36443  pell1qr1  36453  pellqrexplicit  36459  pellfundex  36468  reglogltb  36473  reglogleb  36474  pellfund14  36480  rmspecsqrtnqOLD  36489  rmxycomplete  36500  jm2.24nn  36544  jm2.17b  36546  jm2.17c  36547  jm2.18  36573  jm2.19lem2  36575  jm2.20nn  36582  jm2.16nn0  36589  jm3.1lem2  36603  areaquad  36821  clsk3nimkb  37358  lemuldiv3d  37494  lemuldiv4d  37495  stoweidlem1  38894  stoweidlem11  38904  stoweidlem14  38907  stoweidlem26  38919  stoweidlem34  38927  stoweidlem38  38931  stoweidlem60  38953  fourierdlem52  39051  etransclem38  39165  pfxsuffeqwrdeq  40269  0uhgrsubgr  40503  clwwlksf1  41224  upgr4cycl4dv4e  41352  eupth2lem3lem3  41398  domnmsuppn0  41944  lincvalpr  42001  ldepspr  42056  islindeps2  42066  fldivexpfllog2  42157