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  3847  2nreu  4409  fveqf1o  7306  frrlem12  8296  enfixsn  9077  gruina  10814  grur1  10816  enqeq  10930  muldivdid  11920  recrec  11923  rec11r  11925  divdivdiv  11927  dmdcan  11936  ddcan  11940  rereccl  11944  div2neg  11949  divmuld  12024  divmul2d  12035  divmul3d  12036  divassd  12037  div12d  12038  div23d  12039  divdird  12040  divsubdird  12041  div11d  12042  ltmul12a  12082  ltdiv1  12090  ltrec  12108  lt2msq1  12110  lediv2  12116  supmul1  12195  qbtwnre  13237  xlemul1a  13326  xlemul1  13328  xadd4d  13341  quoremz  13902  quoremnn0ALT  13904  expgt1  14150  nnlesq  14255  expnbnd  14282  expmulnbnd  14285  discr1  14289  facubnd  14350  pfxsuffeqwrdeq  14753  01sqrexlem6  15318  mulcn2  15667  geomulcvg  15949  cvgrat  15956  eftlub  16183  eflegeo  16195  tanhlt1  16234  sin01bnd  16259  cos01bnd  16260  eirrlem  16278  bitsmod  16512  mulgcd  16624  mulgcddvds  16731  prmind2  16761  qnumgt0  16827  pcpremul  16921  fldivp1  16975  pcfaclem  16976  qexpz  16979  prmpwdvds  16982  pockthg  16984  prmreclem1  16994  prmreclem5  16998  4sqlem10  17025  4sqlem12  17034  4sqlem16  17038  4sqlem17  17039  vdwlem3  17061  vdwlem8  17066  vdwlem9  17067  0ram  17098  ramz2  17102  cat1lem  18171  odmulg  19650  dfod2  19658  odf1o1  19666  odf1o2  19667  sylow3lem4  19724  ablsub4  19904  odadd1  19942  odadd2  19943  ablfacrp2  20163  ablfac1b  20166  ablfac1eu  20169  pgpfac1lem3a  20172  pgpfaclem2  20178  ablsimpgfindlem1  20203  chrcong  21707  znrrg  21745  cygznlem1  21746  chpdmatlem3  23027  txdis  23820  txdis1cn  23823  ptunhmeo  23996  qustgplem  24309  blcld  24693  nlmvscnlem2  24873  blcvx  24986  metds0  25039  metdseq0  25043  icopnfcnv  25132  lebnumii  25156  ipcau2  25424  tcphcphlem1  25425  ipcnlem2  25434  csbren  25589  trirn  25590  dyadf  25781  dyadovol  25783  dyaddisjlem  25785  dyadmaxlem  25787  opnmbllem  25791  mbfmulc2lem  25837  mbfi1fseqlem4  25908  mbfi1fseqlem5  25909  mbfi1fseqlem6  25910  itg2mulclem  25936  itg2monolem1  25940  itg2monolem3  25942  itg2cnlem2  25952  itgabs  26025  dvlip  26183  dvlt0  26195  dvcvx  26210  ftc1lem4  26229  dgrcolem2  26462  aaliou3lem2  26537  aaliou3lem9  26544  itgulm  26602  radcnvlem1  26607  abelthlem2  26626  abelthlem7  26632  tangtx  26701  cosne0  26725  cosordlem  26726  tanord1  26733  logdivlti  26816  logcnlem4  26841  logf1o2  26846  cxpcn3lem  26943  cxpaddle  26948  ang180lem2  27006  atanlogsublem  27111  atantan  27119  atanbndlem  27121  atans2  27127  leibpi  27138  log2tlbnd  27141  birthdaylem3  27149  efrlim  27165  jensenlem2  27183  zetacvg  27210  ftalem1  27268  ftalem5  27272  basellem1  27276  basellem4  27279  fsumdvdsdiaglem  27378  dvdsflf1o  27382  fsumfldivdiaglem  27384  ppiub  27399  mersenne  27422  dchrptlem1  27459  bposlem1  27479  bposlem2  27480  bposlem4  27482  lgsdilem  27519  lgseisenlem1  27570  lgseisenlem2  27571  lgseisenlem3  27572  lgsquadlem1  27575  lgsquadlem2  27576  2sqlem3  27615  2sqlem8  27621  2sqlem11  27624  2sqblem  27626  chebbnd1lem2  27665  chebbnd1lem3  27666  rplogsumlem1  27679  rplogsumlem2  27680  dchrisumlem1  27684  dchrmusum2  27689  dchrisum0flblem1  27703  mulog2sumlem1  27729  logdivbnd  27751  pntpbnd1a  27780  pntpbnd1  27781  pntpbnd2  27782  pntlemh  27794  pntlemr  27797  pntlemk  27801  pntlemo  27802  ostth2lem1  27813  ostth2lem2  27829  ostth2lem3  27830  ostth3  27833  noextenddif  27863  noextendlt  27864  noextendgt  27865  nosupbnd1lem3  27905  nosupbnd1lem4  27906  nosupbnd1lem5  27907  nosupbnd1lem6  27908  noinfbnd1lem3  27920  noinfbnd1lem4  27921  noinfbnd1lem5  27922  noinfbnd1lem6  27923  noetasuplem4  27931  madecut  28107  cofcut2  28146  eucliddivs  28600  legov  28885  axsegcon  29308  axpaschlem  29321  0uhgrsubgr  29663  clwwlkf1  30443  upgr4cycl4dv4e  30583  eupth2lem3lem3  30628  nrt2irr  30871  nmblolbii  31198  nmbdoplbi  32423  nmcoplbi  32427  nmophmi  32430  nmbdfnlbi  32448  nmcfnlbi  32451  cnlnadjlem7  32472  nmopcoi  32494  resf1o  33121  receqid  33135  xdivrec  33292  cycpmfvlem  33472  cycpmfv3  33475  lbsdiflsp0  34056  txomap  34264  unitdivcld  34331  measvunilem  34643  measvuni  34645  measssd  34646  measiuns  34648  measinblem  34651  measdivcst  34655  sibfof  34771  oddpwdc  34785  sseqfv1  34820  sseqfv2  34825  probun  34850  totprobd  34857  dstrvprob  34903  actfunsnrndisj  35033  reprsuc  35043  breprexplema  35058  subfaclim  35693  connpconn  35740  cvmliftlem2  35791  cvmliftlem6  35795  cvmliftlem7  35796  cvmliftlem8  35797  cvmliftlem9  35798  cvmliftlem10  35799  snmlff  35834  lineext  36581  hilbert1.1  36659  nn0prpwlem  36866  poimirlem1  38305  opnmbllem0  38340  ismblfin  38345  itgabsnc  38373  ftc1cnnclem  38375  bfplem1  38506  bfp  38508  lfl1  39877  lfladdcl  39878  eqlkr  39906  lkrlsp  39909  atcvrj2b  40239  3dim1  40274  3dim2  40275  llni2  40319  2llnjaN  40373  lvoli3  40384  lvoli2  40388  lncvrelatN  40588  lhpat4N  40851  lhpat3  40853  4atexlemex6  40881  ldilco  40923  ltrnid  40942  ltrnatb  40944  ltrnel  40946  ltrncnvel  40949  ltrncnv  40953  ltrn11at  40954  ltrneq  40956  trlat  40976  trlator0  40978  ltrnnidn  40981  trlid0  40983  trlnidatb  40984  trlnle  40993  trlval3  40994  trlval4  40995  cdlemc2  40999  cdlemc5  41002  cdlemc6  41003  cdlemc  41004  cdlemd2  41006  cdlemd9  41013  cdleme0e  41024  cdleme02N  41029  cdleme0ex1N  41030  cdleme3e  41039  cdleme3g  41041  cdleme3h  41042  cdleme3  41044  cdleme7aa  41049  cdleme7b  41051  cdleme7c  41052  cdleme7d  41053  cdleme7e  41054  cdleme7ga  41055  cdleme7  41056  cdleme9  41060  cdleme16aN  41066  cdleme11c  41068  cdleme11dN  41069  cdleme11e  41070  cdleme11h  41073  cdleme11j  41074  cdleme11k  41075  cdleme12  41078  cdleme21j  41143  cdleme26eALTN  41168  cdleme26f  41170  cdleme26f2  41172  cdlemefrs29bpre0  41203  cdleme35a  41255  cdleme35b  41257  cdleme35c  41258  cdleme35f  41261  cdleme36a  41267  cdleme38m  41270  cdlemeg46rgv  41335  cdlemeg46req  41336  cdlemf  41370  cdlemg2fvlem  41401  cdlemg2l  41410  cdlemg7N  41433  cdlemg12g  41456  cdlemg15  41463  cdlemg17h  41475  cdlemg17  41484  cdlemg19a  41490  cdlemg24  41495  cdlemg37  41496  cdlemg27a  41499  cdlemg31b0N  41501  cdlemg27b  41503  cdlemg31c  41506  cdlemg31d  41507  cdlemg35  41520  trljco  41547  tgrpgrplem  41556  cdlemh2  41623  tendoconid  41636  tendotr  41637  cdlemk35s-id  41745  cdlemk39s-id  41747  cdlemk53b  41763  cdlemk53  41764  cdlemk54  41765  cdleml3N  41785  cdleml5N  41787  tendospcanN  41830  diclss  42000  dihvalcq2  42054  dihord4  42065  dihord5b  42066  dihord5apre  42069  dihmeetlem1N  42097  dihmeetbclemN  42111  dihmeetlem20N  42133  dihmeetALTN  42134  dihatlat  42141  dihatexv  42145  dochkr1  42285  dochkr1OLDN  42286  lcfl7lem  42306  lclkrlem2m  42326  hdmaplna1  42714  hdmaplns1  42715  hdmaplnm1  42716  cxp111d  43136  eldioph2lem1  43524  fphpdo  43577  irrapxlem1  43582  irrapxlem2  43583  irrapxlem3  43584  irrapxlem5  43586  pellexlem2  43590  pell1234qrreccl  43614  pell1234qrmulcl  43615  pell1234qrdich  43621  pell1qr1  43631  pellqrexplicit  43637  pellfundex  43646  reglogltb  43651  reglogleb  43652  pellfund14  43658  rmxycomplete  43677  jm2.24nn  43719  jm2.17b  43721  jm2.17c  43722  jm2.18  43748  jm2.19lem2  43750  jm2.20nn  43757  jm2.16nn0  43764  jm3.1lem2  43778  areaquad  43976  clsk3nimkb  44799  lemuldiv3d  44929  lemuldiv4d  44930  stoweidlem1  46748  stoweidlem11  46758  stoweidlem14  46761  stoweidlem26  46773  stoweidlem34  46781  stoweidlem38  46785  stoweidlem60  46807  fourierdlem52  46905  etransclem38  47019  2tceilhalfelfzo1  48106  reuopreuprim  48308  nprmdvdsfacm1lem4  48408  quad1  48418  requad1  48420  requad2  48421  isubgr3stgrlem1  48764  isubgr3stgrlem3  48766  gpg3kgrtriexlem1  48881  gpg3kgrtriexlem5  48885  domnmsuppn0  49182  lincvalpr  49231  ldepspr  49286  islindeps2  49296  fldivexpfllog2  49378  eenglngeehlnmlem1  49550  eenglngeehlnmlem2  49551  rrx2linest  49555  prsthinc  50275