Theorem syl112anc 1392

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  rmob2  3843  2nreu  4395  fveqf1o  7280  frrlem12  8271  enfixsn  9051  gruina  10769  grur1  10771  enqeq  10885  muldivdid  11878  recrec  11881  rec11r  11883  divdivdiv  11885  dmdcan  11894  ddcan  11898  rereccl  11902  div2neg  11907  divmuld  11982  divmul2d  11993  divmul3d  11994  divassd  11995  div12d  11996  div23d  11997  divdird  11998  divsubdird  11999  div11d  12000  ltmul12a  12040  ltdiv1  12049  ltrec  12067  lt2msq1  12069  lediv2  12075  supmul1  12154  qbtwnre  13195  xlemul1a  13284  xlemul1  13286  xadd4d  13299  quoremz  13858  quoremnn0ALT  13860  expgt1  14106  nnlesq  14211  expnbnd  14238  expmulnbnd  14241  discr1  14245  facubnd  14306  pfxsuffeqwrdeq  14704  01sqrexlem6  15264  mulcn2  15613  geomulcvg  15896  cvgrat  15903  eftlub  16131  eflegeo  16143  tanhlt1  16182  sin01bnd  16207  cos01bnd  16208  eirrlem  16226  bitsmod  16460  mulgcd  16572  mulgcddvds  16679  prmind2  16709  qnumgt0  16775  pcpremul  16869  fldivp1  16923  pcfaclem  16924  qexpz  16927  prmpwdvds  16930  pockthg  16932  prmreclem1  16942  prmreclem5  16946  4sqlem10  16973  4sqlem12  16982  4sqlem16  16986  4sqlem17  16987  vdwlem3  17009  vdwlem8  17014  vdwlem9  17015  0ram  17046  ramz2  17050  cat1lem  18119  odmulg  19586  dfod2  19594  odf1o1  19602  odf1o2  19603  sylow3lem4  19660  ablsub4  19840  odadd1  19878  odadd2  19879  ablfacrp2  20099  ablfac1b  20102  ablfac1eu  20105  pgpfac1lem3a  20108  pgpfaclem2  20114  ablsimpgfindlem1  20139  chrcong  21566  znrrg  21604  cygznlem1  21605  chpdmatlem3  22887  txdis  23679  txdis1cn  23682  ptunhmeo  23855  qustgplem  24168  blcld  24552  nlmvscnlem2  24732  blcvx  24845  metds0  24898  metdseq0  24902  icopnfcnv  24991  lebnumii  25015  ipcau2  25283  tcphcphlem1  25284  ipcnlem2  25293  csbren  25448  trirn  25449  dyadf  25640  dyadovol  25642  dyaddisjlem  25644  dyadmaxlem  25646  opnmbllem  25650  mbfmulc2lem  25696  mbfi1fseqlem4  25767  mbfi1fseqlem5  25768  mbfi1fseqlem6  25769  itg2mulclem  25795  itg2monolem1  25799  itg2monolem3  25801  itg2cnlem2  25811  itgabs  25884  dvlip  26042  dvlt0  26054  dvcvx  26069  ftc1lem4  26088  dgrcolem2  26321  aaliou3lem2  26394  aaliou3lem9  26401  itgulm  26458  radcnvlem1  26463  abelthlem2  26482  abelthlem7  26488  tangtx  26557  cosne0  26581  cosordlem  26582  tanord1  26589  logdivlti  26672  logcnlem4  26697  logf1o2  26702  cxpcn3lem  26799  cxpaddle  26804  ang180lem2  26862  atanlogsublem  26967  atantan  26975  atanbndlem  26977  atans2  26983  leibpi  26994  log2tlbnd  26997  birthdaylem3  27005  efrlim  27021  jensenlem2  27039  zetacvg  27066  ftalem1  27124  ftalem5  27128  basellem1  27132  basellem4  27135  fsumdvdsdiaglem  27234  dvdsflf1o  27238  fsumfldivdiaglem  27240  ppiub  27255  mersenne  27278  dchrptlem1  27315  bposlem1  27335  bposlem2  27336  bposlem4  27338  lgsdilem  27375  lgseisenlem1  27426  lgseisenlem2  27427  lgseisenlem3  27428  lgsquadlem1  27431  lgsquadlem2  27432  2sqlem3  27471  2sqlem8  27477  2sqlem11  27480  2sqblem  27482  chebbnd1lem2  27521  chebbnd1lem3  27522  rplogsumlem1  27535  rplogsumlem2  27536  dchrisumlem1  27540  dchrmusum2  27545  dchrisum0flblem1  27559  mulog2sumlem1  27585  logdivbnd  27607  pntpbnd1a  27636  pntpbnd1  27637  pntpbnd2  27638  pntlemh  27650  pntlemr  27653  pntlemk  27657  pntlemo  27658  ostth2lem1  27669  ostth2lem2  27685  ostth2lem3  27686  ostth3  27689  noextenddif  27719  noextendlt  27720  noextendgt  27721  nosupbnd1lem3  27761  nosupbnd1lem4  27762  nosupbnd1lem5  27763  nosupbnd1lem6  27764  noinfbnd1lem3  27776  noinfbnd1lem4  27777  noinfbnd1lem5  27778  noinfbnd1lem6  27779  noetasuplem4  27787  madecut  27963  cofcut2  28002  eucliddivs  28456  legov  28741  axsegcon  29084  axpaschlem  29097  0uhgrsubgr  29436  clwwlkf1  30207  upgr4cycl4dv4e  30343  eupth2lem3lem3  30388  nrt2irr  30631  nmblolbii  30958  nmbdoplbi  32183  nmcoplbi  32187  nmophmi  32190  nmbdfnlbi  32208  nmcfnlbi  32211  cnlnadjlem7  32232  nmopcoi  32254  resf1o  32892  receqid  32906  xdivrec  33064  cycpmfvlem  33252  cycpmfv3  33255  lbsdiflsp0  33883  txomap  34091  unitdivcld  34158  measvunilem  34469  measvuni  34471  measssd  34472  measiuns  34474  measinblem  34477  measdivcst  34481  sibfof  34597  oddpwdc  34611  sseqfv1  34646  sseqfv2  34651  probun  34676  totprobd  34683  dstrvprob  34729  actfunsnrndisj  34859  reprsuc  34869  breprexplema  34884  subfaclim  35498  connpconn  35545  cvmliftlem2  35596  cvmliftlem6  35600  cvmliftlem7  35601  cvmliftlem8  35602  cvmliftlem9  35603  cvmliftlem10  35604  snmlff  35639  lineext  36386  hilbert1.1  36464  nn0prpwlem  36642  poimirlem1  38080  opnmbllem0  38115  ismblfin  38120  itgabsnc  38148  ftc1cnnclem  38150  bfplem1  38281  bfp  38283  lfl1  39654  lfladdcl  39655  eqlkr  39683  lkrlsp  39686  atcvrj2b  40016  3dim1  40051  3dim2  40052  llni2  40096  2llnjaN  40150  lvoli3  40161  lvoli2  40165  lncvrelatN  40365  lhpat4N  40628  lhpat3  40630  4atexlemex6  40658  ldilco  40700  ltrnid  40719  ltrnatb  40721  ltrnel  40723  ltrncnvel  40726  ltrncnv  40730  ltrn11at  40731  ltrneq  40733  trlat  40753  trlator0  40755  ltrnnidn  40758  trlid0  40760  trlnidatb  40761  trlnle  40770  trlval3  40771  trlval4  40772  cdlemc2  40776  cdlemc5  40779  cdlemc6  40780  cdlemc  40781  cdlemd2  40783  cdlemd9  40790  cdleme0e  40801  cdleme02N  40806  cdleme0ex1N  40807  cdleme3e  40816  cdleme3g  40818  cdleme3h  40819  cdleme3  40821  cdleme7aa  40826  cdleme7b  40828  cdleme7c  40829  cdleme7d  40830  cdleme7e  40831  cdleme7ga  40832  cdleme7  40833  cdleme9  40837  cdleme16aN  40843  cdleme11c  40845  cdleme11dN  40846  cdleme11e  40847  cdleme11h  40850  cdleme11j  40851  cdleme11k  40852  cdleme12  40855  cdleme21j  40920  cdleme26eALTN  40945  cdleme26f  40947  cdleme26f2  40949  cdlemefrs29bpre0  40980  cdleme35a  41032  cdleme35b  41034  cdleme35c  41035  cdleme35f  41038  cdleme36a  41044  cdleme38m  41047  cdlemeg46rgv  41112  cdlemeg46req  41113  cdlemf  41147  cdlemg2fvlem  41178  cdlemg2l  41187  cdlemg7N  41210  cdlemg12g  41233  cdlemg15  41240  cdlemg17h  41252  cdlemg17  41261  cdlemg19a  41267  cdlemg24  41272  cdlemg37  41273  cdlemg27a  41276  cdlemg31b0N  41278  cdlemg27b  41280  cdlemg31c  41283  cdlemg31d  41284  cdlemg35  41297  trljco  41324  tgrpgrplem  41333  cdlemh2  41400  tendoconid  41413  tendotr  41414  cdlemk35s-id  41522  cdlemk39s-id  41524  cdlemk53b  41540  cdlemk53  41541  cdlemk54  41542  cdleml3N  41562  cdleml5N  41564  tendospcanN  41607  diclss  41777  dihvalcq2  41831  dihord4  41842  dihord5b  41843  dihord5apre  41846  dihmeetlem1N  41874  dihmeetbclemN  41888  dihmeetlem20N  41910  dihmeetALTN  41911  dihatlat  41918  dihatexv  41922  dochkr1  42062  dochkr1OLDN  42063  lcfl7lem  42083  lclkrlem2m  42103  hdmaplna1  42491  hdmaplns1  42492  hdmaplnm1  42493  cxp111d  42911  eldioph2lem1  43301  fphpdo  43354  irrapxlem1  43359  irrapxlem2  43360  irrapxlem3  43361  irrapxlem5  43363  pellexlem2  43367  pell1234qrreccl  43391  pell1234qrmulcl  43392  pell1234qrdich  43398  pell1qr1  43408  pellqrexplicit  43414  pellfundex  43423  reglogltb  43428  reglogleb  43429  pellfund14  43435  rmxycomplete  43454  jm2.24nn  43496  jm2.17b  43498  jm2.17c  43499  jm2.18  43525  jm2.19lem2  43527  jm2.20nn  43534  jm2.16nn0  43541  jm3.1lem2  43555  areaquad  43753  clsk3nimkb  44576  lemuldiv3d  44706  lemuldiv4d  44707  stoweidlem1  46535  stoweidlem11  46545  stoweidlem14  46548  stoweidlem26  46560  stoweidlem34  46568  stoweidlem38  46572  stoweidlem60  46594  fourierdlem52  46692  etransclem38  46806  2tceilhalfelfzo1  47890  reuopreuprim  48092  nprmdvdsfacm1lem4  48192  quad1  48202  requad1  48204  requad2  48205  isubgr3stgrlem1  48548  isubgr3stgrlem3  48550  gpg3kgrtriexlem1  48665  gpg3kgrtriexlem5  48669  domnmsuppn0  48951  lincvalpr  49000  ldepspr  49055  islindeps2  49065  fldivexpfllog2  49147  eenglngeehlnmlem1  49319  eenglngeehlnmlem2  49320  rrx2linest  49324  prsthinc  50045