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  37869  opnmbllem0  37904  ismblfin  37909  itgabsnc  37937  ftc1cnnclem  37939  bfplem1  38070  bfp  38072  lfl1  39443  lfladdcl  39444  eqlkr  39472  lkrlsp  39475  atcvrj2b  39805  3dim1  39840  3dim2  39841  llni2  39885  2llnjaN  39939  lvoli3  39950  lvoli2  39954  lncvrelatN  40154  lhpat4N  40417  lhpat3  40419  4atexlemex6  40447  ldilco  40489  ltrnid  40508  ltrnatb  40510  ltrnel  40512  ltrncnvel  40515  ltrncnv  40519  ltrn11at  40520  ltrneq  40522  trlat  40542  trlator0  40544  ltrnnidn  40547  trlid0  40549  trlnidatb  40550  trlnle  40559  trlval3  40560  trlval4  40561  cdlemc2  40565  cdlemc5  40568  cdlemc6  40569  cdlemc  40570  cdlemd2  40572  cdlemd9  40579  cdleme0e  40590  cdleme02N  40595  cdleme0ex1N  40596  cdleme3e  40605  cdleme3g  40607  cdleme3h  40608  cdleme3  40610  cdleme7aa  40615  cdleme7b  40617  cdleme7c  40618  cdleme7d  40619  cdleme7e  40620  cdleme7ga  40621  cdleme7  40622  cdleme9  40626  cdleme16aN  40632  cdleme11c  40634  cdleme11dN  40635  cdleme11e  40636  cdleme11h  40639  cdleme11j  40640  cdleme11k  40641  cdleme12  40644  cdleme21j  40709  cdleme26eALTN  40734  cdleme26f  40736  cdleme26f2  40738  cdlemefrs29bpre0  40769  cdleme35a  40821  cdleme35b  40823  cdleme35c  40824  cdleme35f  40827  cdleme36a  40833  cdleme38m  40836  cdlemeg46rgv  40901  cdlemeg46req  40902  cdlemf  40936  cdlemg2fvlem  40967  cdlemg2l  40976  cdlemg7N  40999  cdlemg12g  41022  cdlemg15  41029  cdlemg17h  41041  cdlemg17  41050  cdlemg19a  41056  cdlemg24  41061  cdlemg37  41062  cdlemg27a  41065  cdlemg31b0N  41067  cdlemg27b  41069  cdlemg31c  41072  cdlemg31d  41073  cdlemg35  41086  trljco  41113  tgrpgrplem  41122  cdlemh2  41189  tendoconid  41202  tendotr  41203  cdlemk35s-id  41311  cdlemk39s-id  41313  cdlemk53b  41329  cdlemk53  41330  cdlemk54  41331  cdleml3N  41351  cdleml5N  41353  tendospcanN  41396  diclss  41566  dihvalcq2  41620  dihord4  41631  dihord5b  41632  dihord5apre  41635  dihmeetlem1N  41663  dihmeetbclemN  41677  dihmeetlem20N  41699  dihmeetALTN  41700  dihatlat  41707  dihatexv  41711  dochkr1  41851  dochkr1OLDN  41852  lcfl7lem  41872  lclkrlem2m  41892  hdmaplna1  42280  hdmaplns1  42281  hdmaplnm1  42282  cxp111d  42709  eldioph2lem1  43114  fphpdo  43171  irrapxlem1  43176  irrapxlem2  43177  irrapxlem3  43178  irrapxlem5  43180  pellexlem2  43184  pell1234qrreccl  43208  pell1234qrmulcl  43209  pell1234qrdich  43215  pell1qr1  43225  pellqrexplicit  43231  pellfundex  43240  reglogltb  43245  reglogleb  43246  pellfund14  43252  rmxycomplete  43271  jm2.24nn  43313  jm2.17b  43315  jm2.17c  43316  jm2.18  43342  jm2.19lem2  43344  jm2.20nn  43351  jm2.16nn0  43358  jm3.1lem2  43372  areaquad  43570  clsk3nimkb  44393  lemuldiv3d  44523  lemuldiv4d  44524  stoweidlem1  46356  stoweidlem11  46366  stoweidlem14  46369  stoweidlem26  46381  stoweidlem34  46389  stoweidlem38  46393  stoweidlem60  46415  fourierdlem52  46513  etransclem38  46627  2tceilhalfelfzo1  47689  reuopreuprim  47883  quad1  47977  requad1  47979  requad2  47980  isubgr3stgrlem1  48323  isubgr3stgrlem3  48325  gpg3kgrtriexlem1  48440  gpg3kgrtriexlem5  48444  domnmsuppn0  48726  lincvalpr  48775  ldepspr  48830  islindeps2  48840  fldivexpfllog2  48922  eenglngeehlnmlem1  49094  eenglngeehlnmlem2  49095  rrx2linest  49099  prsthinc  49820