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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  rmob2  3839  2nreu  4401  fveqf1o  7310  frrlem12  8316  enfixsn  9106  gruina  10904  grur1  10906  enqeq  11020  muldivdid  12012  recrec  12015  rec11r  12017  divdivdiv  12019  dmdcan  12028  ddcan  12032  rereccl  12036  div2neg  12041  divmuld  12116  divmul2d  12127  divmul3d  12128  divassd  12129  div12d  12130  div23d  12131  divdird  12132  divsubdird  12133  div11d  12134  ltmul12a  12174  ltdiv1  12182  ltrec  12200  lt2msq1  12202  lediv2  12208  supmul1  12287  qbtwnre  13330  xlemul1a  13419  xlemul1  13421  xadd4d  13434  quoremz  13996  quoremnn0ALT  13998  expgt1  14244  nnlesq  14350  expnbnd  14377  expmulnbnd  14380  discr1  14384  facubnd  14445  pfxsuffeqwrdeq  14848  01sqrexlem6  15415  mulcn2  15764  geomulcvg  16046  cvgrat  16053  eftlub  16278  eflegeo  16290  tanhlt1  16329  sin01bnd  16354  cos01bnd  16355  eirrlem  16373  bitsmod  16607  mulgcd  16722  mulgcddvds  16831  prmind2  16861  qnumgt0  16927  pcpremul  17022  fldivp1  17076  pcfaclem  17077  qexpz  17080  prmpwdvds  17083  pockthg  17085  prmreclem1  17095  prmreclem5  17099  4sqlem10  17126  4sqlem12  17135  4sqlem16  17139  4sqlem17  17140  vdwlem3  17162  vdwlem8  17167  vdwlem9  17168  0ram  17199  ramz2  17203  cat1lem  18272  odmulg  19771  dfod2  19779  odf1o1  19787  odf1o2  19788  sylow3lem4  19845  ablsub4  20025  odadd1  20063  odadd2  20064  ablfacrp2  20284  ablfac1b  20287  ablfac1eu  20290  pgpfac1lem3a  20293  pgpfaclem2  20299  ablsimpgfindlem1  20324  chrcong  21834  znrrg  21872  cygznlem1  21873  chpdmatlem3  23159  txdis  23952  txdis1cn  23955  ptunhmeo  24128  qustgplem  24441  blcld  24825  nlmvscnlem2  25005  blcvx  25118  metds0  25171  metdseq0  25175  icopnfcnv  25264  lebnumii  25288  ipcau2  25556  tcphcphlem1  25557  ipcnlem2  25566  csbren  25721  trirn  25722  dyadf  25913  dyadovol  25915  dyaddisjlem  25917  dyadmaxlem  25919  opnmbllem  25923  mbfmulc2lem  25969  mbfi1fseqlem4  26040  mbfi1fseqlem5  26041  mbfi1fseqlem6  26042  itg2mulclem  26068  itg2monolem1  26072  itg2monolem3  26074  itg2cnlem2  26084  itgabs  26156  dvlip  26314  dvlt0  26326  dvcvx  26341  ftc1lem4  26360  dgrcolem2  26594  aaliou3lem2  26671  aaliou3lem9  26678  itgulm  26736  radcnvlem1  26741  abelthlem2  26760  abelthlem7  26766  tangtx  26835  cosne0  26858  cosordlem  26859  tanord1  26866  logdivlti  26949  logcnlem4  26974  logf1o2  26979  cxpcn3lem  27076  cxpaddle  27081  ang180lem2  27139  atanlogsublem  27244  atantan  27252  atanbndlem  27254  atans2  27260  leibpi  27271  log2tlbnd  27274  birthdaylem3  27282  efrlim  27298  jensenlem2  27316  zetacvg  27343  ftalem1  27401  ftalem5  27405  basellem1  27409  basellem4  27412  fsumdvdsdiaglem  27511  dvdsflf1o  27515  fsumfldivdiaglem  27517  ppiub  27532  mersenne  27555  dchrptlem1  27592  bposlem1  27612  bposlem2  27613  bposlem4  27615  lgsdilem  27652  lgseisenlem1  27703  lgseisenlem2  27704  lgseisenlem3  27705  lgsquadlem1  27708  lgsquadlem2  27709  2sqlem3  27748  2sqlem8  27754  2sqlem11  27757  2sqblem  27759  chebbnd1lem2  27798  chebbnd1lem3  27799  rplogsumlem1  27812  rplogsumlem2  27813  dchrisumlem1  27817  dchrmusum2  27822  dchrisum0flblem1  27836  mulog2sumlem1  27862  logdivbnd  27884  pntpbnd1a  27913  pntpbnd1  27914  pntpbnd2  27915  pntlemh  27927  pntlemr  27930  pntlemk  27934  pntlemo  27935  ostth2lem1  27946  ostth2lem2  27962  ostth2lem3  27963  ostth3  27966  noextenddif  28026  noextendlt  28027  noextendgt  28028  nosupbnd1lem3  28068  nosupbnd1lem4  28069  nosupbnd1lem5  28070  nosupbnd1lem6  28071  noinfbnd1lem3  28083  noinfbnd1lem4  28084  noinfbnd1lem5  28085  noinfbnd1lem6  28086  noetasuplem4  28094  madecut  28270  cofcut2  28309  eucliddivs  28763  legov  29049  axsegcon  29506  axpaschlem  29519  0uhgrsubgr  29861  clwwlkf1  30641  upgr4cycl4dv4e  30787  eupth2lem3lem3  30832  nrt2irr  31075  nmblolbii  31402  nmbdoplbi  32627  nmcoplbi  32631  nmophmi  32634  nmbdfnlbi  32652  nmcfnlbi  32655  cnlnadjlem7  32676  nmopcoi  32698  resf1o  33365  receqid  33379  xdivrec  33536  cycpmfvlem  33716  cycpmfv3  33719  lbsdiflsp0  34301  txomap  34509  unitdivcld  34576  measvunilem  34888  measvuni  34890  measssd  34891  measiuns  34893  measinblem  34896  measdivcst  34900  sibfof  35015  oddpwdc  35029  sseqfv1  35064  sseqfv2  35069  probun  35094  totprobd  35101  dstrvprob  35147  actfunsnrndisj  35277  reprsuc  35287  breprexplema  35302  subfaclim  35996  connpconn  36043  cvmliftlem2  36094  cvmliftlem6  36098  cvmliftlem7  36099  cvmliftlem8  36100  cvmliftlem9  36101  cvmliftlem10  36102  snmlff  36137  lineext  36884  hilbert1.1  36962  nn0prpwlem  37153  poimirlem1  38583  opnmbllem0  38618  ismblfin  38623  itgabsnc  38651  ftc1cnnclem  38653  bfplem1  38800  bfp  38802  lfl1  40171  lfladdcl  40172  eqlkr  40200  lkrlsp  40203  atcvrj2b  40533  3dim1  40568  3dim2  40569  llni2  40613  2llnjaN  40667  lvoli3  40678  lvoli2  40682  lncvrelatN  40882  lhpat4N  41145  lhpat3  41147  4atexlemex6  41175  ldilco  41217  ltrnid  41236  ltrnatb  41238  ltrnel  41240  ltrncnvel  41243  ltrncnv  41247  ltrn11at  41248  ltrneq  41250  trlat  41270  trlator0  41272  ltrnnidn  41275  trlid0  41277  trlnidatb  41278  trlnle  41287  trlval3  41288  trlval4  41289  cdlemc2  41293  cdlemc5  41296  cdlemc6  41297  cdlemc  41298  cdlemd2  41300  cdlemd9  41307  cdleme0e  41318  cdleme02N  41323  cdleme0ex1N  41324  cdleme3e  41333  cdleme3g  41335  cdleme3h  41336  cdleme3  41338  cdleme7aa  41343  cdleme7b  41345  cdleme7c  41346  cdleme7d  41347  cdleme7e  41348  cdleme7ga  41349  cdleme7  41350  cdleme9  41354  cdleme16aN  41360  cdleme11c  41362  cdleme11dN  41363  cdleme11e  41364  cdleme11h  41367  cdleme11j  41368  cdleme11k  41369  cdleme12  41372  cdleme21j  41437  cdleme26eALTN  41462  cdleme26f  41464  cdleme26f2  41466  cdlemefrs29bpre0  41497  cdleme35a  41549  cdleme35b  41551  cdleme35c  41552  cdleme35f  41555  cdleme36a  41561  cdleme38m  41564  cdlemeg46rgv  41629  cdlemeg46req  41630  cdlemf  41664  cdlemg2fvlem  41695  cdlemg2l  41704  cdlemg7N  41727  cdlemg12g  41750  cdlemg15  41757  cdlemg17h  41769  cdlemg17  41778  cdlemg19a  41784  cdlemg24  41789  cdlemg37  41790  cdlemg27a  41793  cdlemg31b0N  41795  cdlemg27b  41797  cdlemg31c  41800  cdlemg31d  41801  cdlemg35  41814  trljco  41841  tgrpgrplem  41850  cdlemh2  41917  tendoconid  41930  tendotr  41931  cdlemk35s-id  42039  cdlemk39s-id  42041  cdlemk53b  42057  cdlemk53  42058  cdlemk54  42059  cdleml3N  42079  cdleml5N  42081  tendospcanN  42124  diclss  42294  dihvalcq2  42348  dihord4  42359  dihord5b  42360  dihord5apre  42363  dihmeetlem1N  42391  dihmeetbclemN  42405  dihmeetlem20N  42427  dihmeetALTN  42428  dihatlat  42435  dihatexv  42439  dochkr1  42579  dochkr1OLDN  42580  lcfl7lem  42600  lclkrlem2m  42620  hdmaplna1  43008  hdmaplns1  43009  hdmaplnm1  43010  cxp111d  43437  eldioph2lem1  43815  fphpdo  43868  irrapxlem1  43873  irrapxlem2  43874  irrapxlem3  43875  irrapxlem5  43877  pellexlem2  43881  pell1234qrreccl  43905  pell1234qrmulcl  43906  pell1234qrdich  43912  pell1qr1  43922  pellqrexplicit  43928  pellfundex  43937  reglogltb  43942  reglogleb  43943  pellfund14  43949  rmxycomplete  43968  jm2.24nn  44010  jm2.17b  44012  jm2.17c  44013  jm2.18  44039  jm2.19lem2  44041  jm2.20nn  44048  jm2.16nn0  44055  jm3.1lem2  44069  areaquad  44262  clsk3nimkb  45084  lemuldiv3d  45214  lemuldiv4d  45215  stoweidlem1  47055  stoweidlem11  47065  stoweidlem14  47068  stoweidlem26  47080  stoweidlem34  47088  stoweidlem38  47092  stoweidlem60  47114  fourierdlem52  47212  etransclem38  47326  2tceilhalfelfzo1  48450  reuopreuprim  48652  nprmdvdsfacm1lem4  48752  quad1  48762  requad1  48764  requad2  48765  isubgr3stgrlem1  49108  isubgr3stgrlem3  49110  gpg3kgrtriexlem1  49225  gpg3kgrtriexlem5  49229  domnmsuppn0  49525  lincvalpr  49574  ldepspr  49629  islindeps2  49639  fldivexpfllog2  49721  eenglngeehlnmlem1  49893  eenglngeehlnmlem2  49894  rrx2linest  49898  prsthinc  50616