Theorem syl112anc 1376

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 1373	1 ⊢ (𝜑 → 𝜂)

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

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 1088

This theorem is referenced by:  rmob2  3839  2nreu  4393  fveqf1o  7242  frrlem12  8233  enfixsn  9006  gruina  10716  grur1  10718  enqeq  10832  recrec  11825  rec11r  11827  divdivdiv  11829  dmdcan  11838  ddcan  11842  rereccl  11846  div2neg  11851  divmuld  11926  divmul2d  11937  divmul3d  11938  divassd  11939  div12d  11940  div23d  11941  divdird  11942  divsubdird  11943  div11d  11944  ltmul12a  11984  ltdiv1  11993  ltrec  12011  lt2msq1  12013  lediv2  12019  supmul1  12098  qbtwnre  13100  xlemul1a  13189  xlemul1  13191  xadd4d  13204  quoremz  13761  quoremnn0ALT  13763  expgt1  14009  nnlesq  14114  expnbnd  14141  expmulnbnd  14144  discr1  14148  facubnd  14209  pfxsuffeqwrdeq  14607  01sqrexlem6  15156  mulcn2  15505  geomulcvg  15785  cvgrat  15792  eftlub  16020  eflegeo  16032  tanhlt1  16071  sin01bnd  16096  cos01bnd  16097  eirrlem  16115  bitsmod  16349  mulgcd  16461  mulgcddvds  16568  prmind2  16598  qnumgt0  16663  pcpremul  16757  fldivp1  16811  pcfaclem  16812  qexpz  16815  prmpwdvds  16818  pockthg  16820  prmreclem1  16830  prmreclem5  16834  4sqlem10  16861  4sqlem12  16870  4sqlem16  16874  4sqlem17  16875  vdwlem3  16897  vdwlem8  16902  vdwlem9  16903  0ram  16934  ramz2  16938  cat1lem  18005  odmulg  19470  dfod2  19478  odf1o1  19486  odf1o2  19487  sylow3lem4  19544  ablsub4  19724  odadd1  19762  odadd2  19763  ablfacrp2  19983  ablfac1b  19986  ablfac1eu  19989  pgpfac1lem3a  19992  pgpfaclem2  19998  ablsimpgfindlem1  20023  chrcong  21466  znrrg  21504  cygznlem1  21505  chpdmatlem3  22756  txdis  23548  txdis1cn  23551  ptunhmeo  23724  qustgplem  24037  blcld  24421  nlmvscnlem2  24601  blcvx  24714  metds0  24767  metdseq0  24771  icopnfcnv  24868  lebnumii  24893  ipcau2  25162  tcphcphlem1  25163  ipcnlem2  25172  csbren  25327  trirn  25328  dyadf  25520  dyadovol  25522  dyaddisjlem  25524  dyadmaxlem  25526  opnmbllem  25530  mbfmulc2lem  25576  mbfi1fseqlem4  25647  mbfi1fseqlem5  25648  mbfi1fseqlem6  25649  itg2mulclem  25675  itg2monolem1  25679  itg2monolem3  25681  itg2cnlem2  25691  itgabs  25764  dvlip  25926  dvlt0  25938  dvcvx  25953  ftc1lem4  25974  dgrcolem2  26208  aaliou3lem2  26279  aaliou3lem9  26286  itgulm  26345  radcnvlem1  26350  abelthlem2  26370  abelthlem7  26376  tangtx  26442  cosne0  26466  cosordlem  26467  tanord1  26474  logdivlti  26557  logcnlem4  26582  logf1o2  26587  cxpcn3lem  26685  cxpaddle  26690  ang180lem2  26748  atanlogsublem  26853  atantan  26861  atanbndlem  26863  atans2  26869  leibpi  26880  log2tlbnd  26883  birthdaylem3  26891  efrlim  26907  efrlimOLD  26908  jensenlem2  26926  zetacvg  26953  ftalem1  27011  ftalem5  27015  basellem1  27019  basellem4  27022  fsumdvdsdiaglem  27121  dvdsflf1o  27125  fsumfldivdiaglem  27127  ppiub  27143  mersenne  27166  dchrptlem1  27203  bposlem1  27223  bposlem2  27224  bposlem4  27226  lgsdilem  27263  lgseisenlem1  27314  lgseisenlem2  27315  lgseisenlem3  27316  lgsquadlem1  27319  lgsquadlem2  27320  2sqlem3  27359  2sqlem8  27365  2sqlem11  27368  2sqblem  27370  chebbnd1lem2  27409  chebbnd1lem3  27410  rplogsumlem1  27423  rplogsumlem2  27424  dchrisumlem1  27428  dchrmusum2  27433  dchrisum0flblem1  27447  mulog2sumlem1  27473  logdivbnd  27495  pntpbnd1a  27524  pntpbnd1  27525  pntpbnd2  27526  pntlemh  27538  pntlemr  27541  pntlemk  27545  pntlemo  27546  ostth2lem1  27557  ostth2lem2  27573  ostth2lem3  27574  ostth3  27577  noextenddif  27608  noextendlt  27609  noextendgt  27610  nosupbnd1lem3  27650  nosupbnd1lem4  27651  nosupbnd1lem5  27652  nosupbnd1lem6  27653  noinfbnd1lem3  27665  noinfbnd1lem4  27666  noinfbnd1lem5  27667  noinfbnd1lem6  27668  noetasuplem4  27676  madecut  27829  cofcut2  27867  eucliddivs  28302  legov  28564  axsegcon  28907  axpaschlem  28920  0uhgrsubgr  29259  clwwlkf1  30031  upgr4cycl4dv4e  30167  eupth2lem3lem3  30212  nrt2irr  30455  nmblolbii  30781  nmbdoplbi  32006  nmcoplbi  32010  nmophmi  32013  nmbdfnlbi  32031  nmcfnlbi  32034  cnlnadjlem7  32055  nmopcoi  32077  resf1o  32717  muldivdid  32728  receqid  32732  xdivrec  32914  cycpmfvlem  33088  cycpmfv3  33091  lbsdiflsp0  33660  txomap  33868  unitdivcld  33935  measvunilem  34246  measvuni  34248  measssd  34249  measiuns  34251  measinblem  34254  measdivcst  34258  sibfof  34374  oddpwdc  34388  sseqfv1  34423  sseqfv2  34428  probun  34453  totprobd  34460  dstrvprob  34506  actfunsnrndisj  34639  reprsuc  34649  breprexplema  34664  subfaclim  35253  connpconn  35300  cvmliftlem2  35351  cvmliftlem6  35355  cvmliftlem7  35356  cvmliftlem8  35357  cvmliftlem9  35358  cvmliftlem10  35359  snmlff  35394  lineext  36141  hilbert1.1  36219  nn0prpwlem  36387  poimirlem1  37681  opnmbllem0  37716  ismblfin  37721  itgabsnc  37749  ftc1cnnclem  37751  bfplem1  37882  bfp  37884  lfl1  39189  lfladdcl  39190  eqlkr  39218  lkrlsp  39221  atcvrj2b  39551  3dim1  39586  3dim2  39587  llni2  39631  2llnjaN  39685  lvoli3  39696  lvoli2  39700  lncvrelatN  39900  lhpat4N  40163  lhpat3  40165  4atexlemex6  40193  ldilco  40235  ltrnid  40254  ltrnatb  40256  ltrnel  40258  ltrncnvel  40261  ltrncnv  40265  ltrn11at  40266  ltrneq  40268  trlat  40288  trlator0  40290  ltrnnidn  40293  trlid0  40295  trlnidatb  40296  trlnle  40305  trlval3  40306  trlval4  40307  cdlemc2  40311  cdlemc5  40314  cdlemc6  40315  cdlemc  40316  cdlemd2  40318  cdlemd9  40325  cdleme0e  40336  cdleme02N  40341  cdleme0ex1N  40342  cdleme3e  40351  cdleme3g  40353  cdleme3h  40354  cdleme3  40356  cdleme7aa  40361  cdleme7b  40363  cdleme7c  40364  cdleme7d  40365  cdleme7e  40366  cdleme7ga  40367  cdleme7  40368  cdleme9  40372  cdleme16aN  40378  cdleme11c  40380  cdleme11dN  40381  cdleme11e  40382  cdleme11h  40385  cdleme11j  40386  cdleme11k  40387  cdleme12  40390  cdleme21j  40455  cdleme26eALTN  40480  cdleme26f  40482  cdleme26f2  40484  cdlemefrs29bpre0  40515  cdleme35a  40567  cdleme35b  40569  cdleme35c  40570  cdleme35f  40573  cdleme36a  40579  cdleme38m  40582  cdlemeg46rgv  40647  cdlemeg46req  40648  cdlemf  40682  cdlemg2fvlem  40713  cdlemg2l  40722  cdlemg7N  40745  cdlemg12g  40768  cdlemg15  40775  cdlemg17h  40787  cdlemg17  40796  cdlemg19a  40802  cdlemg24  40807  cdlemg37  40808  cdlemg27a  40811  cdlemg31b0N  40813  cdlemg27b  40815  cdlemg31c  40818  cdlemg31d  40819  cdlemg35  40832  trljco  40859  tgrpgrplem  40868  cdlemh2  40935  tendoconid  40948  tendotr  40949  cdlemk35s-id  41057  cdlemk39s-id  41059  cdlemk53b  41075  cdlemk53  41076  cdlemk54  41077  cdleml3N  41097  cdleml5N  41099  tendospcanN  41142  diclss  41312  dihvalcq2  41366  dihord4  41377  dihord5b  41378  dihord5apre  41381  dihmeetlem1N  41409  dihmeetbclemN  41423  dihmeetlem20N  41445  dihmeetALTN  41446  dihatlat  41453  dihatexv  41457  dochkr1  41597  dochkr1OLDN  41598  lcfl7lem  41618  lclkrlem2m  41638  hdmaplna1  42026  hdmaplns1  42027  hdmaplnm1  42028  cxp111d  42460  eldioph2lem1  42877  fphpdo  42934  irrapxlem1  42939  irrapxlem2  42940  irrapxlem3  42941  irrapxlem5  42943  pellexlem2  42947  pell1234qrreccl  42971  pell1234qrmulcl  42972  pell1234qrdich  42978  pell1qr1  42988  pellqrexplicit  42994  pellfundex  43003  reglogltb  43008  reglogleb  43009  pellfund14  43015  rmxycomplete  43034  jm2.24nn  43076  jm2.17b  43078  jm2.17c  43079  jm2.18  43105  jm2.19lem2  43107  jm2.20nn  43114  jm2.16nn0  43121  jm3.1lem2  43135  areaquad  43333  clsk3nimkb  44157  lemuldiv3d  44287  lemuldiv4d  44288  stoweidlem1  46123  stoweidlem11  46133  stoweidlem14  46136  stoweidlem26  46148  stoweidlem34  46156  stoweidlem38  46160  stoweidlem60  46182  fourierdlem52  46280  etransclem38  46394  2tceilhalfelfzo1  47456  reuopreuprim  47650  quad1  47744  requad1  47746  requad2  47747  isubgr3stgrlem1  48090  isubgr3stgrlem3  48092  gpg3kgrtriexlem1  48207  gpg3kgrtriexlem5  48211  domnmsuppn0  48493  lincvalpr  48543  ldepspr  48598  islindeps2  48608  fldivexpfllog2  48690  eenglngeehlnmlem1  48862  eenglngeehlnmlem2  48863  rrx2linest  48867  prsthinc  49589