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  3840  2nreu  4402  fveqf1o  7303  frrlem12  8296  enfixsn  9084  gruina  10827  grur1  10829  enqeq  10943  muldivdid  11933  recrec  11936  rec11r  11938  divdivdiv  11940  dmdcan  11949  ddcan  11953  rereccl  11957  div2neg  11962  divmuld  12037  divmul2d  12048  divmul3d  12049  divassd  12050  div12d  12051  div23d  12052  divdird  12053  divsubdird  12054  div11d  12055  ltmul12a  12095  ltdiv1  12103  ltrec  12121  lt2msq1  12123  lediv2  12129  supmul1  12208  qbtwnre  13251  xlemul1a  13340  xlemul1  13342  xadd4d  13355  quoremz  13916  quoremnn0ALT  13918  expgt1  14164  nnlesq  14269  expnbnd  14296  expmulnbnd  14299  discr1  14303  facubnd  14364  pfxsuffeqwrdeq  14767  01sqrexlem6  15334  mulcn2  15683  geomulcvg  15965  cvgrat  15972  eftlub  16197  eflegeo  16209  tanhlt1  16248  sin01bnd  16273  cos01bnd  16274  eirrlem  16292  bitsmod  16526  mulgcd  16638  mulgcddvds  16745  prmind2  16775  qnumgt0  16841  pcpremul  16935  fldivp1  16989  pcfaclem  16990  qexpz  16993  prmpwdvds  16996  pockthg  16998  prmreclem1  17008  prmreclem5  17012  4sqlem10  17039  4sqlem12  17048  4sqlem16  17052  4sqlem17  17053  vdwlem3  17075  vdwlem8  17080  vdwlem9  17081  0ram  17112  ramz2  17116  cat1lem  18185  odmulg  19683  dfod2  19691  odf1o1  19699  odf1o2  19700  sylow3lem4  19757  ablsub4  19937  odadd1  19975  odadd2  19976  ablfacrp2  20196  ablfac1b  20199  ablfac1eu  20202  pgpfac1lem3a  20205  pgpfaclem2  20211  ablsimpgfindlem1  20236  chrcong  21740  znrrg  21778  cygznlem1  21779  chpdmatlem3  23065  txdis  23858  txdis1cn  23861  ptunhmeo  24034  qustgplem  24347  blcld  24731  nlmvscnlem2  24911  blcvx  25024  metds0  25077  metdseq0  25081  icopnfcnv  25170  lebnumii  25194  ipcau2  25462  tcphcphlem1  25463  ipcnlem2  25472  csbren  25627  trirn  25628  dyadf  25819  dyadovol  25821  dyaddisjlem  25823  dyadmaxlem  25825  opnmbllem  25829  mbfmulc2lem  25875  mbfi1fseqlem4  25946  mbfi1fseqlem5  25947  mbfi1fseqlem6  25948  itg2mulclem  25974  itg2monolem1  25978  itg2monolem3  25980  itg2cnlem2  25990  itgabs  26062  dvlip  26220  dvlt0  26232  dvcvx  26247  ftc1lem4  26266  dgrcolem2  26500  aaliou3lem2  26579  aaliou3lem9  26586  itgulm  26644  radcnvlem1  26649  abelthlem2  26668  abelthlem7  26674  tangtx  26743  cosne0  26766  cosordlem  26767  tanord1  26774  logdivlti  26857  logcnlem4  26882  logf1o2  26887  cxpcn3lem  26984  cxpaddle  26989  ang180lem2  27047  atanlogsublem  27152  atantan  27160  atanbndlem  27162  atans2  27168  leibpi  27179  log2tlbnd  27182  birthdaylem3  27190  efrlim  27206  jensenlem2  27224  zetacvg  27251  ftalem1  27309  ftalem5  27313  basellem1  27317  basellem4  27320  fsumdvdsdiaglem  27419  dvdsflf1o  27423  fsumfldivdiaglem  27425  ppiub  27440  mersenne  27463  dchrptlem1  27500  bposlem1  27520  bposlem2  27521  bposlem4  27523  lgsdilem  27560  lgseisenlem1  27611  lgseisenlem2  27612  lgseisenlem3  27613  lgsquadlem1  27616  lgsquadlem2  27617  2sqlem3  27656  2sqlem8  27662  2sqlem11  27665  2sqblem  27667  chebbnd1lem2  27706  chebbnd1lem3  27707  rplogsumlem1  27720  rplogsumlem2  27721  dchrisumlem1  27725  dchrmusum2  27730  dchrisum0flblem1  27744  mulog2sumlem1  27770  logdivbnd  27792  pntpbnd1a  27821  pntpbnd1  27822  pntpbnd2  27823  pntlemh  27835  pntlemr  27838  pntlemk  27842  pntlemo  27843  ostth2lem1  27854  ostth2lem2  27870  ostth2lem3  27871  ostth3  27874  noextenddif  27904  noextendlt  27905  noextendgt  27906  nosupbnd1lem3  27946  nosupbnd1lem4  27947  nosupbnd1lem5  27948  nosupbnd1lem6  27949  noinfbnd1lem3  27961  noinfbnd1lem4  27962  noinfbnd1lem5  27963  noinfbnd1lem6  27964  noetasuplem4  27972  madecut  28148  cofcut2  28187  eucliddivs  28641  legov  28927  axsegcon  29384  axpaschlem  29397  0uhgrsubgr  29739  clwwlkf1  30519  upgr4cycl4dv4e  30665  eupth2lem3lem3  30710  nrt2irr  30953  nmblolbii  31280  nmbdoplbi  32505  nmcoplbi  32509  nmophmi  32512  nmbdfnlbi  32530  nmcfnlbi  32533  cnlnadjlem7  32554  nmopcoi  32576  resf1o  33201  receqid  33215  xdivrec  33372  cycpmfvlem  33552  cycpmfv3  33555  lbsdiflsp0  34136  txomap  34344  unitdivcld  34411  measvunilem  34723  measvuni  34725  measssd  34726  measiuns  34728  measinblem  34731  measdivcst  34735  sibfof  34851  oddpwdc  34865  sseqfv1  34900  sseqfv2  34905  probun  34930  totprobd  34937  dstrvprob  34983  actfunsnrndisj  35113  reprsuc  35123  breprexplema  35138  subfaclim  35767  connpconn  35814  cvmliftlem2  35865  cvmliftlem6  35869  cvmliftlem7  35870  cvmliftlem8  35871  cvmliftlem9  35872  cvmliftlem10  35873  snmlff  35908  lineext  36656  hilbert1.1  36734  nn0prpwlem  36941  poimirlem1  38370  opnmbllem0  38405  ismblfin  38410  itgabsnc  38438  ftc1cnnclem  38440  bfplem1  38572  bfp  38574  lfl1  39943  lfladdcl  39944  eqlkr  39972  lkrlsp  39975  atcvrj2b  40305  3dim1  40340  3dim2  40341  llni2  40385  2llnjaN  40439  lvoli3  40450  lvoli2  40454  lncvrelatN  40654  lhpat4N  40917  lhpat3  40919  4atexlemex6  40947  ldilco  40989  ltrnid  41008  ltrnatb  41010  ltrnel  41012  ltrncnvel  41015  ltrncnv  41019  ltrn11at  41020  ltrneq  41022  trlat  41042  trlator0  41044  ltrnnidn  41047  trlid0  41049  trlnidatb  41050  trlnle  41059  trlval3  41060  trlval4  41061  cdlemc2  41065  cdlemc5  41068  cdlemc6  41069  cdlemc  41070  cdlemd2  41072  cdlemd9  41079  cdleme0e  41090  cdleme02N  41095  cdleme0ex1N  41096  cdleme3e  41105  cdleme3g  41107  cdleme3h  41108  cdleme3  41110  cdleme7aa  41115  cdleme7b  41117  cdleme7c  41118  cdleme7d  41119  cdleme7e  41120  cdleme7ga  41121  cdleme7  41122  cdleme9  41126  cdleme16aN  41132  cdleme11c  41134  cdleme11dN  41135  cdleme11e  41136  cdleme11h  41139  cdleme11j  41140  cdleme11k  41141  cdleme12  41144  cdleme21j  41209  cdleme26eALTN  41234  cdleme26f  41236  cdleme26f2  41238  cdlemefrs29bpre0  41269  cdleme35a  41321  cdleme35b  41323  cdleme35c  41324  cdleme35f  41327  cdleme36a  41333  cdleme38m  41336  cdlemeg46rgv  41401  cdlemeg46req  41402  cdlemf  41436  cdlemg2fvlem  41467  cdlemg2l  41476  cdlemg7N  41499  cdlemg12g  41522  cdlemg15  41529  cdlemg17h  41541  cdlemg17  41550  cdlemg19a  41556  cdlemg24  41561  cdlemg37  41562  cdlemg27a  41565  cdlemg31b0N  41567  cdlemg27b  41569  cdlemg31c  41572  cdlemg31d  41573  cdlemg35  41586  trljco  41613  tgrpgrplem  41622  cdlemh2  41689  tendoconid  41702  tendotr  41703  cdlemk35s-id  41811  cdlemk39s-id  41813  cdlemk53b  41829  cdlemk53  41830  cdlemk54  41831  cdleml3N  41851  cdleml5N  41853  tendospcanN  41896  diclss  42066  dihvalcq2  42120  dihord4  42131  dihord5b  42132  dihord5apre  42135  dihmeetlem1N  42163  dihmeetbclemN  42177  dihmeetlem20N  42199  dihmeetALTN  42200  dihatlat  42207  dihatexv  42211  dochkr1  42351  dochkr1OLDN  42352  lcfl7lem  42372  lclkrlem2m  42392  hdmaplna1  42780  hdmaplns1  42781  hdmaplnm1  42782  cxp111d  43217  eldioph2lem1  43605  fphpdo  43658  irrapxlem1  43663  irrapxlem2  43664  irrapxlem3  43665  irrapxlem5  43667  pellexlem2  43671  pell1234qrreccl  43695  pell1234qrmulcl  43696  pell1234qrdich  43702  pell1qr1  43712  pellqrexplicit  43718  pellfundex  43727  reglogltb  43732  reglogleb  43733  pellfund14  43739  rmxycomplete  43758  jm2.24nn  43800  jm2.17b  43802  jm2.17c  43803  jm2.18  43829  jm2.19lem2  43831  jm2.20nn  43838  jm2.16nn0  43845  jm3.1lem2  43859  areaquad  44057  clsk3nimkb  44880  lemuldiv3d  45010  lemuldiv4d  45011  stoweidlem1  46829  stoweidlem11  46839  stoweidlem14  46842  stoweidlem26  46854  stoweidlem34  46862  stoweidlem38  46866  stoweidlem60  46888  fourierdlem52  46986  etransclem38  47100  2tceilhalfelfzo1  48224  reuopreuprim  48426  nprmdvdsfacm1lem4  48526  quad1  48536  requad1  48538  requad2  48539  isubgr3stgrlem1  48882  isubgr3stgrlem3  48884  gpg3kgrtriexlem1  48999  gpg3kgrtriexlem5  49003  domnmsuppn0  49299  lincvalpr  49348  ldepspr  49403  islindeps2  49413  fldivexpfllog2  49495  eenglngeehlnmlem1  49667  eenglngeehlnmlem2  49668  rrx2linest  49672  prsthinc  50390