Theorem syl112anc 1374

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  rmob2  3914  2nreu  4467  fveqf1o  7338  frrlem12  8338  enfixsn  9147  gruina  10887  grur1  10889  enqeq  11003  recrec  11991  rec11r  11993  divdivdiv  11995  dmdcan  12004  ddcan  12008  rereccl  12012  div2neg  12017  divmuld  12092  divmul2d  12103  divmul3d  12104  divassd  12105  div12d  12106  div23d  12107  divdird  12108  divsubdird  12109  div11d  12110  ltmul12a  12150  ltdiv1  12159  ltrec  12177  lt2msq1  12179  lediv2  12185  supmul1  12264  qbtwnre  13261  xlemul1a  13350  xlemul1  13352  xadd4d  13365  quoremz  13906  quoremnn0ALT  13908  expgt1  14151  nnlesq  14254  expnbnd  14281  expmulnbnd  14284  discr1  14288  facubnd  14349  pfxsuffeqwrdeq  14746  01sqrexlem6  15296  mulcn2  15642  geomulcvg  15924  cvgrat  15931  eftlub  16157  eflegeo  16169  tanhlt1  16208  sin01bnd  16233  cos01bnd  16234  eirrlem  16252  bitsmod  16482  mulgcd  16595  mulgcddvds  16702  prmind2  16732  qnumgt0  16797  pcpremul  16890  fldivp1  16944  pcfaclem  16945  qexpz  16948  prmpwdvds  16951  pockthg  16953  prmreclem1  16963  prmreclem5  16967  4sqlem10  16994  4sqlem12  17003  4sqlem16  17007  4sqlem17  17008  vdwlem3  17030  vdwlem8  17035  vdwlem9  17036  0ram  17067  ramz2  17071  cat1lem  18163  odmulg  19598  dfod2  19606  odf1o1  19614  odf1o2  19615  sylow3lem4  19672  ablsub4  19852  odadd1  19890  odadd2  19891  ablfacrp2  20111  ablfac1b  20114  ablfac1eu  20117  pgpfac1lem3a  20120  pgpfaclem2  20126  ablsimpgfindlem1  20151  chrcong  21565  znrrg  21607  cygznlem1  21608  chpdmatlem3  22867  txdis  23661  txdis1cn  23664  ptunhmeo  23837  qustgplem  24150  blcld  24539  nlmvscnlem2  24727  blcvx  24839  metds0  24891  metdseq0  24895  icopnfcnv  24992  lebnumii  25017  ipcau2  25287  tcphcphlem1  25288  ipcnlem2  25297  csbren  25452  trirn  25453  dyadf  25645  dyadovol  25647  dyaddisjlem  25649  dyadmaxlem  25651  opnmbllem  25655  mbfmulc2lem  25701  mbfi1fseqlem4  25773  mbfi1fseqlem5  25774  mbfi1fseqlem6  25775  itg2mulclem  25801  itg2monolem1  25805  itg2monolem3  25807  itg2cnlem2  25817  itgabs  25890  dvlip  26052  dvlt0  26064  dvcvx  26079  ftc1lem4  26100  dgrcolem2  26334  aaliou3lem2  26403  aaliou3lem9  26410  itgulm  26469  radcnvlem1  26474  abelthlem2  26494  abelthlem7  26500  tangtx  26565  cosne0  26589  cosordlem  26590  tanord1  26597  logdivlti  26680  logcnlem4  26705  logf1o2  26710  cxpcn3lem  26808  cxpaddle  26813  ang180lem2  26871  atanlogsublem  26976  atantan  26984  atanbndlem  26986  atans2  26992  leibpi  27003  log2tlbnd  27006  birthdaylem3  27014  efrlim  27030  efrlimOLD  27031  jensenlem2  27049  zetacvg  27076  ftalem1  27134  ftalem5  27138  basellem1  27142  basellem4  27145  fsumdvdsdiaglem  27244  dvdsflf1o  27248  fsumfldivdiaglem  27250  ppiub  27266  mersenne  27289  dchrptlem1  27326  bposlem1  27346  bposlem2  27347  bposlem4  27349  lgsdilem  27386  lgseisenlem1  27437  lgseisenlem2  27438  lgseisenlem3  27439  lgsquadlem1  27442  lgsquadlem2  27443  2sqlem3  27482  2sqlem8  27488  2sqlem11  27491  2sqblem  27493  chebbnd1lem2  27532  chebbnd1lem3  27533  rplogsumlem1  27546  rplogsumlem2  27547  dchrisumlem1  27551  dchrmusum2  27556  dchrisum0flblem1  27570  mulog2sumlem1  27596  logdivbnd  27618  pntpbnd1a  27647  pntpbnd1  27648  pntpbnd2  27649  pntlemh  27661  pntlemr  27664  pntlemk  27668  pntlemo  27669  ostth2lem1  27680  ostth2lem2  27696  ostth2lem3  27697  ostth3  27700  noextenddif  27731  noextendlt  27732  noextendgt  27733  nosupbnd1lem3  27773  nosupbnd1lem4  27774  nosupbnd1lem5  27775  nosupbnd1lem6  27776  noinfbnd1lem3  27788  noinfbnd1lem4  27789  noinfbnd1lem5  27790  noinfbnd1lem6  27791  noetasuplem4  27799  madecut  27939  cofcut2  27974  legov  28611  axsegcon  28960  axpaschlem  28973  0uhgrsubgr  29314  clwwlkf1  30081  upgr4cycl4dv4e  30217  eupth2lem3lem3  30262  nrt2irr  30505  nmblolbii  30831  nmbdoplbi  32056  nmcoplbi  32060  nmophmi  32063  nmbdfnlbi  32081  nmcfnlbi  32084  cnlnadjlem7  32105  nmopcoi  32127  resf1o  32744  muldivdid  32754  xdivrec  32891  cycpmfvlem  33105  cycpmfv3  33108  lbsdiflsp0  33639  txomap  33780  unitdivcld  33847  measvunilem  34176  measvuni  34178  measssd  34179  measiuns  34181  measinblem  34184  measdivcst  34188  sibfof  34305  oddpwdc  34319  sseqfv1  34354  sseqfv2  34359  probun  34384  totprobd  34391  dstrvprob  34436  actfunsnrndisj  34582  reprsuc  34592  breprexplema  34607  subfaclim  35156  connpconn  35203  cvmliftlem2  35254  cvmliftlem6  35258  cvmliftlem7  35259  cvmliftlem8  35260  cvmliftlem9  35261  cvmliftlem10  35262  snmlff  35297  lineext  36040  hilbert1.1  36118  nn0prpwlem  36288  poimirlem1  37581  opnmbllem0  37616  ismblfin  37621  itgabsnc  37649  ftc1cnnclem  37651  bfplem1  37782  bfp  37784  lfl1  39026  lfladdcl  39027  eqlkr  39055  lkrlsp  39058  atcvrj2b  39389  3dim1  39424  3dim2  39425  llni2  39469  2llnjaN  39523  lvoli3  39534  lvoli2  39538  lncvrelatN  39738  lhpat4N  40001  lhpat3  40003  4atexlemex6  40031  ldilco  40073  ltrnid  40092  ltrnatb  40094  ltrnel  40096  ltrncnvel  40099  ltrncnv  40103  ltrn11at  40104  ltrneq  40106  trlat  40126  trlator0  40128  ltrnnidn  40131  trlid0  40133  trlnidatb  40134  trlnle  40143  trlval3  40144  trlval4  40145  cdlemc2  40149  cdlemc5  40152  cdlemc6  40153  cdlemc  40154  cdlemd2  40156  cdlemd9  40163  cdleme0e  40174  cdleme02N  40179  cdleme0ex1N  40180  cdleme3e  40189  cdleme3g  40191  cdleme3h  40192  cdleme3  40194  cdleme7aa  40199  cdleme7b  40201  cdleme7c  40202  cdleme7d  40203  cdleme7e  40204  cdleme7ga  40205  cdleme7  40206  cdleme9  40210  cdleme16aN  40216  cdleme11c  40218  cdleme11dN  40219  cdleme11e  40220  cdleme11h  40223  cdleme11j  40224  cdleme11k  40225  cdleme12  40228  cdleme21j  40293  cdleme26eALTN  40318  cdleme26f  40320  cdleme26f2  40322  cdlemefrs29bpre0  40353  cdleme35a  40405  cdleme35b  40407  cdleme35c  40408  cdleme35f  40411  cdleme36a  40417  cdleme38m  40420  cdlemeg46rgv  40485  cdlemeg46req  40486  cdlemf  40520  cdlemg2fvlem  40551  cdlemg2l  40560  cdlemg7N  40583  cdlemg12g  40606  cdlemg15  40613  cdlemg17h  40625  cdlemg17  40634  cdlemg19a  40640  cdlemg24  40645  cdlemg37  40646  cdlemg27a  40649  cdlemg31b0N  40651  cdlemg27b  40653  cdlemg31c  40656  cdlemg31d  40657  cdlemg35  40670  trljco  40697  tgrpgrplem  40706  cdlemh2  40773  tendoconid  40786  tendotr  40787  cdlemk35s-id  40895  cdlemk39s-id  40897  cdlemk53b  40913  cdlemk53  40914  cdlemk54  40915  cdleml3N  40935  cdleml5N  40937  tendospcanN  40980  diclss  41150  dihvalcq2  41204  dihord4  41215  dihord5b  41216  dihord5apre  41219  dihmeetlem1N  41247  dihmeetbclemN  41261  dihmeetlem20N  41283  dihmeetALTN  41284  dihatlat  41291  dihatexv  41295  dochkr1  41435  dochkr1OLDN  41436  lcfl7lem  41456  lclkrlem2m  41476  hdmaplna1  41864  hdmaplns1  41865  hdmaplnm1  41866  cxp111d  42330  eldioph2lem1  42716  fphpdo  42773  irrapxlem1  42778  irrapxlem2  42779  irrapxlem3  42780  irrapxlem5  42782  pellexlem2  42786  pell1234qrreccl  42810  pell1234qrmulcl  42811  pell1234qrdich  42817  pell1qr1  42827  pellqrexplicit  42833  pellfundex  42842  reglogltb  42847  reglogleb  42848  pellfund14  42854  rmxycomplete  42874  jm2.24nn  42916  jm2.17b  42918  jm2.17c  42919  jm2.18  42945  jm2.19lem2  42947  jm2.20nn  42954  jm2.16nn0  42961  jm3.1lem2  42975  areaquad  43177  clsk3nimkb  44002  lemuldiv3d  44132  lemuldiv4d  44133  stoweidlem1  45922  stoweidlem11  45932  stoweidlem14  45935  stoweidlem26  45947  stoweidlem34  45955  stoweidlem38  45959  stoweidlem60  45981  fourierdlem52  46079  etransclem38  46193  reuopreuprim  47400  quad1  47494  requad1  47496  requad2  47497  domnmsuppn0  48094  lincvalpr  48147  ldepspr  48202  islindeps2  48212  fldivexpfllog2  48299  eenglngeehlnmlem1  48471  eenglngeehlnmlem2  48472  rrx2linest  48476  prsthinc  48721