Theorem syl112anc 1377

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 1374	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  3844  2nreu  4398  fveqf1o  7258  frrlem12  8249  enfixsn  9026  gruina  10741  grur1  10743  enqeq  10857  recrec  11850  rec11r  11852  divdivdiv  11854  dmdcan  11863  ddcan  11867  rereccl  11871  div2neg  11876  divmuld  11951  divmul2d  11962  divmul3d  11963  divassd  11964  div12d  11965  div23d  11966  divdird  11967  divsubdird  11968  div11d  11969  ltmul12a  12009  ltdiv1  12018  ltrec  12036  lt2msq1  12038  lediv2  12044  supmul1  12123  qbtwnre  13126  xlemul1a  13215  xlemul1  13217  xadd4d  13230  quoremz  13787  quoremnn0ALT  13789  expgt1  14035  nnlesq  14140  expnbnd  14167  expmulnbnd  14170  discr1  14174  facubnd  14235  pfxsuffeqwrdeq  14633  01sqrexlem6  15182  mulcn2  15531  geomulcvg  15811  cvgrat  15818  eftlub  16046  eflegeo  16058  tanhlt1  16097  sin01bnd  16122  cos01bnd  16123  eirrlem  16141  bitsmod  16375  mulgcd  16487  mulgcddvds  16594  prmind2  16624  qnumgt0  16689  pcpremul  16783  fldivp1  16837  pcfaclem  16838  qexpz  16841  prmpwdvds  16844  pockthg  16846  prmreclem1  16856  prmreclem5  16860  4sqlem10  16887  4sqlem12  16896  4sqlem16  16900  4sqlem17  16901  vdwlem3  16923  vdwlem8  16928  vdwlem9  16929  0ram  16960  ramz2  16964  cat1lem  18032  odmulg  19497  dfod2  19505  odf1o1  19513  odf1o2  19514  sylow3lem4  19571  ablsub4  19751  odadd1  19789  odadd2  19790  ablfacrp2  20010  ablfac1b  20013  ablfac1eu  20016  pgpfac1lem3a  20019  pgpfaclem2  20025  ablsimpgfindlem1  20050  chrcong  21494  znrrg  21532  cygznlem1  21533  chpdmatlem3  22796  txdis  23588  txdis1cn  23591  ptunhmeo  23764  qustgplem  24077  blcld  24461  nlmvscnlem2  24641  blcvx  24754  metds0  24807  metdseq0  24811  icopnfcnv  24908  lebnumii  24933  ipcau2  25202  tcphcphlem1  25203  ipcnlem2  25212  csbren  25367  trirn  25368  dyadf  25560  dyadovol  25562  dyaddisjlem  25564  dyadmaxlem  25566  opnmbllem  25570  mbfmulc2lem  25616  mbfi1fseqlem4  25687  mbfi1fseqlem5  25688  mbfi1fseqlem6  25689  itg2mulclem  25715  itg2monolem1  25719  itg2monolem3  25721  itg2cnlem2  25731  itgabs  25804  dvlip  25966  dvlt0  25978  dvcvx  25993  ftc1lem4  26014  dgrcolem2  26248  aaliou3lem2  26319  aaliou3lem9  26326  itgulm  26385  radcnvlem1  26390  abelthlem2  26410  abelthlem7  26416  tangtx  26482  cosne0  26506  cosordlem  26507  tanord1  26514  logdivlti  26597  logcnlem4  26622  logf1o2  26627  cxpcn3lem  26725  cxpaddle  26730  ang180lem2  26788  atanlogsublem  26893  atantan  26901  atanbndlem  26903  atans2  26909  leibpi  26920  log2tlbnd  26923  birthdaylem3  26931  efrlim  26947  efrlimOLD  26948  jensenlem2  26966  zetacvg  26993  ftalem1  27051  ftalem5  27055  basellem1  27059  basellem4  27062  fsumdvdsdiaglem  27161  dvdsflf1o  27165  fsumfldivdiaglem  27167  ppiub  27183  mersenne  27206  dchrptlem1  27243  bposlem1  27263  bposlem2  27264  bposlem4  27266  lgsdilem  27303  lgseisenlem1  27354  lgseisenlem2  27355  lgseisenlem3  27356  lgsquadlem1  27359  lgsquadlem2  27360  2sqlem3  27399  2sqlem8  27405  2sqlem11  27408  2sqblem  27410  chebbnd1lem2  27449  chebbnd1lem3  27450  rplogsumlem1  27463  rplogsumlem2  27464  dchrisumlem1  27468  dchrmusum2  27473  dchrisum0flblem1  27487  mulog2sumlem1  27513  logdivbnd  27535  pntpbnd1a  27564  pntpbnd1  27565  pntpbnd2  27566  pntlemh  27578  pntlemr  27581  pntlemk  27585  pntlemo  27586  ostth2lem1  27597  ostth2lem2  27613  ostth2lem3  27614  ostth3  27617  noextenddif  27648  noextendlt  27649  noextendgt  27650  nosupbnd1lem3  27690  nosupbnd1lem4  27691  nosupbnd1lem5  27692  nosupbnd1lem6  27693  noinfbnd1lem3  27705  noinfbnd1lem4  27706  noinfbnd1lem5  27707  noinfbnd1lem6  27708  noetasuplem4  27716  madecut  27891  cofcut2  27930  eucliddivs  28384  legov  28669  axsegcon  29012  axpaschlem  29025  0uhgrsubgr  29364  clwwlkf1  30136  upgr4cycl4dv4e  30272  eupth2lem3lem3  30317  nrt2irr  30560  nmblolbii  30886  nmbdoplbi  32111  nmcoplbi  32115  nmophmi  32118  nmbdfnlbi  32136  nmcfnlbi  32139  cnlnadjlem7  32160  nmopcoi  32182  resf1o  32819  muldivdid  32830  receqid  32834  xdivrec  33018  cycpmfvlem  33205  cycpmfv3  33208  lbsdiflsp0  33803  txomap  34011  unitdivcld  34078  measvunilem  34389  measvuni  34391  measssd  34392  measiuns  34394  measinblem  34397  measdivcst  34401  sibfof  34517  oddpwdc  34531  sseqfv1  34566  sseqfv2  34571  probun  34596  totprobd  34603  dstrvprob  34649  actfunsnrndisj  34782  reprsuc  34792  breprexplema  34807  subfaclim  35401  connpconn  35448  cvmliftlem2  35499  cvmliftlem6  35503  cvmliftlem7  35504  cvmliftlem8  35505  cvmliftlem9  35506  cvmliftlem10  35507  snmlff  35542  lineext  36289  hilbert1.1  36367  nn0prpwlem  36535  poimirlem1  37866  opnmbllem0  37901  ismblfin  37906  itgabsnc  37934  ftc1cnnclem  37936  bfplem1  38067  bfp  38069  lfl1  39440  lfladdcl  39441  eqlkr  39469  lkrlsp  39472  atcvrj2b  39802  3dim1  39837  3dim2  39838  llni2  39882  2llnjaN  39936  lvoli3  39947  lvoli2  39951  lncvrelatN  40151  lhpat4N  40414  lhpat3  40416  4atexlemex6  40444  ldilco  40486  ltrnid  40505  ltrnatb  40507  ltrnel  40509  ltrncnvel  40512  ltrncnv  40516  ltrn11at  40517  ltrneq  40519  trlat  40539  trlator0  40541  ltrnnidn  40544  trlid0  40546  trlnidatb  40547  trlnle  40556  trlval3  40557  trlval4  40558  cdlemc2  40562  cdlemc5  40565  cdlemc6  40566  cdlemc  40567  cdlemd2  40569  cdlemd9  40576  cdleme0e  40587  cdleme02N  40592  cdleme0ex1N  40593  cdleme3e  40602  cdleme3g  40604  cdleme3h  40605  cdleme3  40607  cdleme7aa  40612  cdleme7b  40614  cdleme7c  40615  cdleme7d  40616  cdleme7e  40617  cdleme7ga  40618  cdleme7  40619  cdleme9  40623  cdleme16aN  40629  cdleme11c  40631  cdleme11dN  40632  cdleme11e  40633  cdleme11h  40636  cdleme11j  40637  cdleme11k  40638  cdleme12  40641  cdleme21j  40706  cdleme26eALTN  40731  cdleme26f  40733  cdleme26f2  40735  cdlemefrs29bpre0  40766  cdleme35a  40818  cdleme35b  40820  cdleme35c  40821  cdleme35f  40824  cdleme36a  40830  cdleme38m  40833  cdlemeg46rgv  40898  cdlemeg46req  40899  cdlemf  40933  cdlemg2fvlem  40964  cdlemg2l  40973  cdlemg7N  40996  cdlemg12g  41019  cdlemg15  41026  cdlemg17h  41038  cdlemg17  41047  cdlemg19a  41053  cdlemg24  41058  cdlemg37  41059  cdlemg27a  41062  cdlemg31b0N  41064  cdlemg27b  41066  cdlemg31c  41069  cdlemg31d  41070  cdlemg35  41083  trljco  41110  tgrpgrplem  41119  cdlemh2  41186  tendoconid  41199  tendotr  41200  cdlemk35s-id  41308  cdlemk39s-id  41310  cdlemk53b  41326  cdlemk53  41327  cdlemk54  41328  cdleml3N  41348  cdleml5N  41350  tendospcanN  41393  diclss  41563  dihvalcq2  41617  dihord4  41628  dihord5b  41629  dihord5apre  41632  dihmeetlem1N  41660  dihmeetbclemN  41674  dihmeetlem20N  41696  dihmeetALTN  41697  dihatlat  41704  dihatexv  41708  dochkr1  41848  dochkr1OLDN  41849  lcfl7lem  41869  lclkrlem2m  41889  hdmaplna1  42277  hdmaplns1  42278  hdmaplnm1  42279  cxp111d  42706  eldioph2lem1  43111  fphpdo  43168  irrapxlem1  43173  irrapxlem2  43174  irrapxlem3  43175  irrapxlem5  43177  pellexlem2  43181  pell1234qrreccl  43205  pell1234qrmulcl  43206  pell1234qrdich  43212  pell1qr1  43222  pellqrexplicit  43228  pellfundex  43237  reglogltb  43242  reglogleb  43243  pellfund14  43249  rmxycomplete  43268  jm2.24nn  43310  jm2.17b  43312  jm2.17c  43313  jm2.18  43339  jm2.19lem2  43341  jm2.20nn  43348  jm2.16nn0  43355  jm3.1lem2  43369  areaquad  43567  clsk3nimkb  44390  lemuldiv3d  44520  lemuldiv4d  44521  stoweidlem1  46353  stoweidlem11  46363  stoweidlem14  46366  stoweidlem26  46378  stoweidlem34  46386  stoweidlem38  46390  stoweidlem60  46412  fourierdlem52  46510  etransclem38  46624  2tceilhalfelfzo1  47686  reuopreuprim  47880  quad1  47974  requad1  47976  requad2  47977  isubgr3stgrlem1  48320  isubgr3stgrlem3  48322  gpg3kgrtriexlem1  48437  gpg3kgrtriexlem5  48441  domnmsuppn0  48723  lincvalpr  48772  ldepspr  48827  islindeps2  48837  fldivexpfllog2  48919  eenglngeehlnmlem1  49091  eenglngeehlnmlem2  49092  rrx2linest  49096  prsthinc  49817