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  3867  2nreu  4419  fveqf1o  7294  frrlem12  8294  enfixsn  9093  gruina  10830  grur1  10832  enqeq  10946  recrec  11936  rec11r  11938  divdivdiv  11940  dmdcan  11949  ddcan  11953  rereccl  11957  div2neg  11962  divmuld  12037  divmul2d  12048  divmul3d  12049  divassd  12050  div12d  12051  div23d  12052  divdird  12053  divsubdird  12054  div11d  12055  ltmul12a  12095  ltdiv1  12104  ltrec  12122  lt2msq1  12124  lediv2  12130  supmul1  12209  qbtwnre  13213  xlemul1a  13302  xlemul1  13304  xadd4d  13317  quoremz  13870  quoremnn0ALT  13872  expgt1  14116  nnlesq  14221  expnbnd  14248  expmulnbnd  14251  discr1  14255  facubnd  14316  pfxsuffeqwrdeq  14714  01sqrexlem6  15264  mulcn2  15610  geomulcvg  15890  cvgrat  15897  eftlub  16125  eflegeo  16137  tanhlt1  16176  sin01bnd  16201  cos01bnd  16202  eirrlem  16220  bitsmod  16453  mulgcd  16565  mulgcddvds  16672  prmind2  16702  qnumgt0  16767  pcpremul  16861  fldivp1  16915  pcfaclem  16916  qexpz  16919  prmpwdvds  16922  pockthg  16924  prmreclem1  16934  prmreclem5  16938  4sqlem10  16965  4sqlem12  16974  4sqlem16  16978  4sqlem17  16979  vdwlem3  17001  vdwlem8  17006  vdwlem9  17007  0ram  17038  ramz2  17042  cat1lem  18107  odmulg  19535  dfod2  19543  odf1o1  19551  odf1o2  19552  sylow3lem4  19609  ablsub4  19789  odadd1  19827  odadd2  19828  ablfacrp2  20048  ablfac1b  20051  ablfac1eu  20054  pgpfac1lem3a  20057  pgpfaclem2  20063  ablsimpgfindlem1  20088  chrcong  21486  znrrg  21524  cygznlem1  21525  chpdmatlem3  22776  txdis  23568  txdis1cn  23571  ptunhmeo  23744  qustgplem  24057  blcld  24442  nlmvscnlem2  24622  blcvx  24735  metds0  24788  metdseq0  24792  icopnfcnv  24889  lebnumii  24914  ipcau2  25184  tcphcphlem1  25185  ipcnlem2  25194  csbren  25349  trirn  25350  dyadf  25542  dyadovol  25544  dyaddisjlem  25546  dyadmaxlem  25548  opnmbllem  25552  mbfmulc2lem  25598  mbfi1fseqlem4  25669  mbfi1fseqlem5  25670  mbfi1fseqlem6  25671  itg2mulclem  25697  itg2monolem1  25701  itg2monolem3  25703  itg2cnlem2  25713  itgabs  25786  dvlip  25948  dvlt0  25960  dvcvx  25975  ftc1lem4  25996  dgrcolem2  26230  aaliou3lem2  26301  aaliou3lem9  26308  itgulm  26367  radcnvlem1  26372  abelthlem2  26392  abelthlem7  26398  tangtx  26464  cosne0  26488  cosordlem  26489  tanord1  26496  logdivlti  26579  logcnlem4  26604  logf1o2  26609  cxpcn3lem  26707  cxpaddle  26712  ang180lem2  26770  atanlogsublem  26875  atantan  26883  atanbndlem  26885  atans2  26891  leibpi  26902  log2tlbnd  26905  birthdaylem3  26913  efrlim  26929  efrlimOLD  26930  jensenlem2  26948  zetacvg  26975  ftalem1  27033  ftalem5  27037  basellem1  27041  basellem4  27044  fsumdvdsdiaglem  27143  dvdsflf1o  27147  fsumfldivdiaglem  27149  ppiub  27165  mersenne  27188  dchrptlem1  27225  bposlem1  27245  bposlem2  27246  bposlem4  27248  lgsdilem  27285  lgseisenlem1  27336  lgseisenlem2  27337  lgseisenlem3  27338  lgsquadlem1  27341  lgsquadlem2  27342  2sqlem3  27381  2sqlem8  27387  2sqlem11  27390  2sqblem  27392  chebbnd1lem2  27431  chebbnd1lem3  27432  rplogsumlem1  27445  rplogsumlem2  27446  dchrisumlem1  27450  dchrmusum2  27455  dchrisum0flblem1  27469  mulog2sumlem1  27495  logdivbnd  27517  pntpbnd1a  27546  pntpbnd1  27547  pntpbnd2  27548  pntlemh  27560  pntlemr  27563  pntlemk  27567  pntlemo  27568  ostth2lem1  27579  ostth2lem2  27595  ostth2lem3  27596  ostth3  27599  noextenddif  27630  noextendlt  27631  noextendgt  27632  nosupbnd1lem3  27672  nosupbnd1lem4  27673  nosupbnd1lem5  27674  nosupbnd1lem6  27675  noinfbnd1lem3  27687  noinfbnd1lem4  27688  noinfbnd1lem5  27689  noinfbnd1lem6  27690  noetasuplem4  27698  madecut  27838  cofcut2  27873  legov  28510  axsegcon  28852  axpaschlem  28865  0uhgrsubgr  29204  clwwlkf1  29976  upgr4cycl4dv4e  30112  eupth2lem3lem3  30157  nrt2irr  30400  nmblolbii  30726  nmbdoplbi  31951  nmcoplbi  31955  nmophmi  31958  nmbdfnlbi  31976  nmcfnlbi  31979  cnlnadjlem7  32000  nmopcoi  32022  resf1o  32653  muldivdid  32664  receqid  32668  xdivrec  32847  cycpmfvlem  33069  cycpmfv3  33072  lbsdiflsp0  33612  txomap  33811  unitdivcld  33878  measvunilem  34189  measvuni  34191  measssd  34192  measiuns  34194  measinblem  34197  measdivcst  34201  sibfof  34318  oddpwdc  34332  sseqfv1  34367  sseqfv2  34372  probun  34397  totprobd  34404  dstrvprob  34450  actfunsnrndisj  34583  reprsuc  34593  breprexplema  34608  subfaclim  35156  connpconn  35203  cvmliftlem2  35254  cvmliftlem6  35258  cvmliftlem7  35259  cvmliftlem8  35260  cvmliftlem9  35261  cvmliftlem10  35262  snmlff  35297  lineext  36040  hilbert1.1  36118  nn0prpwlem  36286  poimirlem1  37591  opnmbllem0  37626  ismblfin  37631  itgabsnc  37659  ftc1cnnclem  37661  bfplem1  37792  bfp  37794  lfl1  39034  lfladdcl  39035  eqlkr  39063  lkrlsp  39066  atcvrj2b  39397  3dim1  39432  3dim2  39433  llni2  39477  2llnjaN  39531  lvoli3  39542  lvoli2  39546  lncvrelatN  39746  lhpat4N  40009  lhpat3  40011  4atexlemex6  40039  ldilco  40081  ltrnid  40100  ltrnatb  40102  ltrnel  40104  ltrncnvel  40107  ltrncnv  40111  ltrn11at  40112  ltrneq  40114  trlat  40134  trlator0  40136  ltrnnidn  40139  trlid0  40141  trlnidatb  40142  trlnle  40151  trlval3  40152  trlval4  40153  cdlemc2  40157  cdlemc5  40160  cdlemc6  40161  cdlemc  40162  cdlemd2  40164  cdlemd9  40171  cdleme0e  40182  cdleme02N  40187  cdleme0ex1N  40188  cdleme3e  40197  cdleme3g  40199  cdleme3h  40200  cdleme3  40202  cdleme7aa  40207  cdleme7b  40209  cdleme7c  40210  cdleme7d  40211  cdleme7e  40212  cdleme7ga  40213  cdleme7  40214  cdleme9  40218  cdleme16aN  40224  cdleme11c  40226  cdleme11dN  40227  cdleme11e  40228  cdleme11h  40231  cdleme11j  40232  cdleme11k  40233  cdleme12  40236  cdleme21j  40301  cdleme26eALTN  40326  cdleme26f  40328  cdleme26f2  40330  cdlemefrs29bpre0  40361  cdleme35a  40413  cdleme35b  40415  cdleme35c  40416  cdleme35f  40419  cdleme36a  40425  cdleme38m  40428  cdlemeg46rgv  40493  cdlemeg46req  40494  cdlemf  40528  cdlemg2fvlem  40559  cdlemg2l  40568  cdlemg7N  40591  cdlemg12g  40614  cdlemg15  40621  cdlemg17h  40633  cdlemg17  40642  cdlemg19a  40648  cdlemg24  40653  cdlemg37  40654  cdlemg27a  40657  cdlemg31b0N  40659  cdlemg27b  40661  cdlemg31c  40664  cdlemg31d  40665  cdlemg35  40678  trljco  40705  tgrpgrplem  40714  cdlemh2  40781  tendoconid  40794  tendotr  40795  cdlemk35s-id  40903  cdlemk39s-id  40905  cdlemk53b  40921  cdlemk53  40922  cdlemk54  40923  cdleml3N  40943  cdleml5N  40945  tendospcanN  40988  diclss  41158  dihvalcq2  41212  dihord4  41223  dihord5b  41224  dihord5apre  41227  dihmeetlem1N  41255  dihmeetbclemN  41269  dihmeetlem20N  41291  dihmeetALTN  41292  dihatlat  41299  dihatexv  41303  dochkr1  41443  dochkr1OLDN  41444  lcfl7lem  41464  lclkrlem2m  41484  hdmaplna1  41872  hdmaplns1  41873  hdmaplnm1  41874  cxp111d  42338  eldioph2lem1  42730  fphpdo  42787  irrapxlem1  42792  irrapxlem2  42793  irrapxlem3  42794  irrapxlem5  42796  pellexlem2  42800  pell1234qrreccl  42824  pell1234qrmulcl  42825  pell1234qrdich  42831  pell1qr1  42841  pellqrexplicit  42847  pellfundex  42856  reglogltb  42861  reglogleb  42862  pellfund14  42868  rmxycomplete  42888  jm2.24nn  42930  jm2.17b  42932  jm2.17c  42933  jm2.18  42959  jm2.19lem2  42961  jm2.20nn  42968  jm2.16nn0  42975  jm3.1lem2  42989  areaquad  43187  clsk3nimkb  44011  lemuldiv3d  44141  lemuldiv4d  44142  stoweidlem1  45978  stoweidlem11  45988  stoweidlem14  45991  stoweidlem26  46003  stoweidlem34  46011  stoweidlem38  46015  stoweidlem60  46037  fourierdlem52  46135  etransclem38  46249  2tceilhalfelfzo1  47309  reuopreuprim  47488  quad1  47582  requad1  47584  requad2  47585  isubgr3stgrlem1  47926  isubgr3stgrlem3  47928  gpg3kgrtriexlem1  48033  gpg3kgrtriexlem5  48037  domnmsuppn0  48292  lincvalpr  48342  ldepspr  48397  islindeps2  48407  fldivexpfllog2  48493  eenglngeehlnmlem1  48665  eenglngeehlnmlem2  48666  rrx2linest  48670  prsthinc  49298