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

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1089

This theorem is referenced by:  rmob2  3886  2nreu  4441  fveqf1o  7303  frrlem12  8284  enfixsn  9083  gruina  10815  grur1  10817  enqeq  10931  recrec  11913  rec11r  11915  divdivdiv  11917  dmdcan  11926  ddcan  11930  rereccl  11934  div2neg  11939  divmuld  12014  divmul2d  12025  divmul3d  12026  divassd  12027  div12d  12028  div23d  12029  divdird  12030  divsubdird  12031  div11d  12032  ltmul12a  12072  ltdiv1  12080  ltrec  12098  lt2msq1  12100  lediv2  12106  supmul1  12185  qbtwnre  13180  xlemul1a  13269  xlemul1  13271  xadd4d  13284  quoremz  13822  quoremnn0ALT  13824  expgt1  14068  nnlesq  14171  expnbnd  14197  expmulnbnd  14200  discr1  14204  facubnd  14262  pfxsuffeqwrdeq  14650  01sqrexlem6  15196  mulcn2  15542  geomulcvg  15824  cvgrat  15831  eftlub  16054  eflegeo  16066  tanhlt1  16105  sin01bnd  16130  cos01bnd  16131  eirrlem  16149  bitsmod  16379  mulgcd  16492  mulgcddvds  16594  prmind2  16624  qnumgt0  16688  pcpremul  16778  fldivp1  16832  pcfaclem  16833  qexpz  16836  prmpwdvds  16839  pockthg  16841  prmreclem1  16851  prmreclem5  16855  4sqlem10  16882  4sqlem12  16891  4sqlem16  16895  4sqlem17  16896  vdwlem3  16918  vdwlem8  16923  vdwlem9  16924  0ram  16955  ramz2  16959  cat1lem  18048  odmulg  19426  dfod2  19434  odf1o1  19442  odf1o2  19443  sylow3lem4  19500  ablsub4  19680  odadd1  19718  odadd2  19719  ablfacrp2  19939  ablfac1b  19942  ablfac1eu  19945  pgpfac1lem3a  19948  pgpfaclem2  19954  ablsimpgfindlem1  19979  chrcong  21087  znrrg  21127  cygznlem1  21128  chpdmatlem3  22349  txdis  23143  txdis1cn  23146  ptunhmeo  23319  qustgplem  23632  blcld  24021  nlmvscnlem2  24209  blcvx  24321  metds0  24373  metdseq0  24377  icopnfcnv  24465  lebnumii  24489  ipcau2  24758  tcphcphlem1  24759  ipcnlem2  24768  csbren  24923  trirn  24924  dyadf  25115  dyadovol  25117  dyaddisjlem  25119  dyadmaxlem  25121  opnmbllem  25125  mbfmulc2lem  25171  mbfi1fseqlem4  25243  mbfi1fseqlem5  25244  mbfi1fseqlem6  25245  itg2mulclem  25271  itg2monolem1  25275  itg2monolem3  25277  itg2cnlem2  25287  itgabs  25359  dvlip  25517  dvlt0  25529  dvcvx  25544  ftc1lem4  25563  dgrcolem2  25795  aaliou3lem2  25863  aaliou3lem9  25870  itgulm  25927  radcnvlem1  25932  abelthlem2  25951  abelthlem7  25957  tangtx  26022  cosne0  26045  cosordlem  26046  tanord1  26053  logdivlti  26135  logcnlem4  26160  logf1o2  26165  cxpcn3lem  26262  cxpaddle  26267  ang180lem2  26322  atanlogsublem  26427  atantan  26435  atanbndlem  26437  atans2  26443  leibpi  26454  log2tlbnd  26457  birthdaylem3  26465  efrlim  26481  jensenlem2  26499  zetacvg  26526  ftalem1  26584  ftalem5  26588  basellem1  26592  basellem4  26595  fsumdvdsdiaglem  26694  dvdsflf1o  26698  fsumfldivdiaglem  26700  ppiub  26714  mersenne  26737  dchrptlem1  26774  bposlem1  26794  bposlem2  26795  bposlem4  26797  lgsdilem  26834  lgseisenlem1  26885  lgseisenlem2  26886  lgseisenlem3  26887  lgsquadlem1  26890  lgsquadlem2  26891  2sqlem3  26930  2sqlem8  26936  2sqlem11  26939  2sqblem  26941  chebbnd1lem2  26980  chebbnd1lem3  26981  rplogsumlem1  26994  rplogsumlem2  26995  dchrisumlem1  26999  dchrmusum2  27004  dchrisum0flblem1  27018  mulog2sumlem1  27044  logdivbnd  27066  pntpbnd1a  27095  pntpbnd1  27096  pntpbnd2  27097  pntlemh  27109  pntlemr  27112  pntlemk  27116  pntlemo  27117  ostth2lem1  27128  ostth2lem2  27144  ostth2lem3  27145  ostth3  27148  noextenddif  27178  noextendlt  27179  noextendgt  27180  nosupbnd1lem3  27220  nosupbnd1lem4  27221  nosupbnd1lem5  27222  nosupbnd1lem6  27223  noinfbnd1lem3  27235  noinfbnd1lem4  27236  noinfbnd1lem5  27237  noinfbnd1lem6  27238  noetasuplem4  27246  madecut  27385  cofcut2  27418  legov  27874  axsegcon  28223  axpaschlem  28236  0uhgrsubgr  28574  clwwlkf1  29340  upgr4cycl4dv4e  29476  eupth2lem3lem3  29521  nrt2irr  29764  nmblolbii  30090  nmbdoplbi  31315  nmcoplbi  31319  nmophmi  31322  nmbdfnlbi  31340  nmcfnlbi  31343  cnlnadjlem7  31364  nmopcoi  31386  resf1o  31993  xdivrec  32131  cycpmfvlem  32312  cycpmfv3  32315  lbsdiflsp0  32770  txomap  32883  unitdivcld  32950  measvunilem  33279  measvuni  33281  measssd  33282  measiuns  33284  measinblem  33287  measdivcst  33291  sibfof  33408  oddpwdc  33422  sseqfv1  33457  sseqfv2  33462  probun  33487  totprobd  33494  dstrvprob  33539  actfunsnrndisj  33686  reprsuc  33696  breprexplema  33711  subfaclim  34248  connpconn  34295  cvmliftlem2  34346  cvmliftlem6  34350  cvmliftlem7  34351  cvmliftlem8  34352  cvmliftlem9  34353  cvmliftlem10  34354  snmlff  34389  lineext  35117  hilbert1.1  35195  nn0prpwlem  35293  poimirlem1  36575  opnmbllem0  36610  ismblfin  36615  itgabsnc  36643  ftc1cnnclem  36645  bfplem1  36776  bfp  36778  lfl1  38026  lfladdcl  38027  eqlkr  38055  lkrlsp  38058  atcvrj2b  38389  3dim1  38424  3dim2  38425  llni2  38469  2llnjaN  38523  lvoli3  38534  lvoli2  38538  lncvrelatN  38738  lhpat4N  39001  lhpat3  39003  4atexlemex6  39031  ldilco  39073  ltrnid  39092  ltrnatb  39094  ltrnel  39096  ltrncnvel  39099  ltrncnv  39103  ltrn11at  39104  ltrneq  39106  trlat  39126  trlator0  39128  ltrnnidn  39131  trlid0  39133  trlnidatb  39134  trlnle  39143  trlval3  39144  trlval4  39145  cdlemc2  39149  cdlemc5  39152  cdlemc6  39153  cdlemc  39154  cdlemd2  39156  cdlemd9  39163  cdleme0e  39174  cdleme02N  39179  cdleme0ex1N  39180  cdleme3e  39189  cdleme3g  39191  cdleme3h  39192  cdleme3  39194  cdleme7aa  39199  cdleme7b  39201  cdleme7c  39202  cdleme7d  39203  cdleme7e  39204  cdleme7ga  39205  cdleme7  39206  cdleme9  39210  cdleme16aN  39216  cdleme11c  39218  cdleme11dN  39219  cdleme11e  39220  cdleme11h  39223  cdleme11j  39224  cdleme11k  39225  cdleme12  39228  cdleme21j  39293  cdleme26eALTN  39318  cdleme26f  39320  cdleme26f2  39322  cdlemefrs29bpre0  39353  cdleme35a  39405  cdleme35b  39407  cdleme35c  39408  cdleme35f  39411  cdleme36a  39417  cdleme38m  39420  cdlemeg46rgv  39485  cdlemeg46req  39486  cdlemf  39520  cdlemg2fvlem  39551  cdlemg2l  39560  cdlemg7N  39583  cdlemg12g  39606  cdlemg15  39613  cdlemg17h  39625  cdlemg17  39634  cdlemg19a  39640  cdlemg24  39645  cdlemg37  39646  cdlemg27a  39649  cdlemg31b0N  39651  cdlemg27b  39653  cdlemg31c  39656  cdlemg31d  39657  cdlemg35  39670  trljco  39697  tgrpgrplem  39706  cdlemh2  39773  tendoconid  39786  tendotr  39787  cdlemk35s-id  39895  cdlemk39s-id  39897  cdlemk53b  39913  cdlemk53  39914  cdlemk54  39915  cdleml3N  39935  cdleml5N  39937  tendospcanN  39980  diclss  40150  dihvalcq2  40204  dihord4  40215  dihord5b  40216  dihord5apre  40219  dihmeetlem1N  40247  dihmeetbclemN  40261  dihmeetlem20N  40283  dihmeetALTN  40284  dihatlat  40291  dihatexv  40295  dochkr1  40435  dochkr1OLDN  40436  lcfl7lem  40456  lclkrlem2m  40476  hdmaplna1  40864  hdmaplns1  40865  hdmaplnm1  40866  eldioph2lem1  41580  fphpdo  41637  irrapxlem1  41642  irrapxlem2  41643  irrapxlem3  41644  irrapxlem5  41646  pellexlem2  41650  pell1234qrreccl  41674  pell1234qrmulcl  41675  pell1234qrdich  41681  pell1qr1  41691  pellqrexplicit  41697  pellfundex  41706  reglogltb  41711  reglogleb  41712  pellfund14  41718  rmxycomplete  41738  jm2.24nn  41780  jm2.17b  41782  jm2.17c  41783  jm2.18  41809  jm2.19lem2  41811  jm2.20nn  41818  jm2.16nn0  41825  jm3.1lem2  41839  areaquad  42047  clsk3nimkb  42873  lemuldiv3d  43004  lemuldiv4d  43005  stoweidlem1  44796  stoweidlem11  44806  stoweidlem14  44809  stoweidlem26  44821  stoweidlem34  44829  stoweidlem38  44833  stoweidlem60  44855  fourierdlem52  44953  etransclem38  45067  reuopreuprim  46273  quad1  46367  requad1  46369  requad2  46370  domnmsuppn0  47124  lincvalpr  47177  ldepspr  47232  islindeps2  47242  fldivexpfllog2  47329  eenglngeehlnmlem1  47501  eenglngeehlnmlem2  47502  rrx2linest  47506  prsthinc  47752