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  3842  2nreu  4396  fveqf1o  7248  frrlem12  8239  enfixsn  9014  gruina  10729  grur1  10731  enqeq  10845  recrec  11838  rec11r  11840  divdivdiv  11842  dmdcan  11851  ddcan  11855  rereccl  11859  div2neg  11864  divmuld  11939  divmul2d  11950  divmul3d  11951  divassd  11952  div12d  11953  div23d  11954  divdird  11955  divsubdird  11956  div11d  11957  ltmul12a  11997  ltdiv1  12006  ltrec  12024  lt2msq1  12026  lediv2  12032  supmul1  12111  qbtwnre  13114  xlemul1a  13203  xlemul1  13205  xadd4d  13218  quoremz  13775  quoremnn0ALT  13777  expgt1  14023  nnlesq  14128  expnbnd  14155  expmulnbnd  14158  discr1  14162  facubnd  14223  pfxsuffeqwrdeq  14621  01sqrexlem6  15170  mulcn2  15519  geomulcvg  15799  cvgrat  15806  eftlub  16034  eflegeo  16046  tanhlt1  16085  sin01bnd  16110  cos01bnd  16111  eirrlem  16129  bitsmod  16363  mulgcd  16475  mulgcddvds  16582  prmind2  16612  qnumgt0  16677  pcpremul  16771  fldivp1  16825  pcfaclem  16826  qexpz  16829  prmpwdvds  16832  pockthg  16834  prmreclem1  16844  prmreclem5  16848  4sqlem10  16875  4sqlem12  16884  4sqlem16  16888  4sqlem17  16889  vdwlem3  16911  vdwlem8  16916  vdwlem9  16917  0ram  16948  ramz2  16952  cat1lem  18020  odmulg  19485  dfod2  19493  odf1o1  19501  odf1o2  19502  sylow3lem4  19559  ablsub4  19739  odadd1  19777  odadd2  19778  ablfacrp2  19998  ablfac1b  20001  ablfac1eu  20004  pgpfac1lem3a  20007  pgpfaclem2  20013  ablsimpgfindlem1  20038  chrcong  21482  znrrg  21520  cygznlem1  21521  chpdmatlem3  22784  txdis  23576  txdis1cn  23579  ptunhmeo  23752  qustgplem  24065  blcld  24449  nlmvscnlem2  24629  blcvx  24742  metds0  24795  metdseq0  24799  icopnfcnv  24896  lebnumii  24921  ipcau2  25190  tcphcphlem1  25191  ipcnlem2  25200  csbren  25355  trirn  25356  dyadf  25548  dyadovol  25550  dyaddisjlem  25552  dyadmaxlem  25554  opnmbllem  25558  mbfmulc2lem  25604  mbfi1fseqlem4  25675  mbfi1fseqlem5  25676  mbfi1fseqlem6  25677  itg2mulclem  25703  itg2monolem1  25707  itg2monolem3  25709  itg2cnlem2  25719  itgabs  25792  dvlip  25954  dvlt0  25966  dvcvx  25981  ftc1lem4  26002  dgrcolem2  26236  aaliou3lem2  26307  aaliou3lem9  26314  itgulm  26373  radcnvlem1  26378  abelthlem2  26398  abelthlem7  26404  tangtx  26470  cosne0  26494  cosordlem  26495  tanord1  26502  logdivlti  26585  logcnlem4  26610  logf1o2  26615  cxpcn3lem  26713  cxpaddle  26718  ang180lem2  26776  atanlogsublem  26881  atantan  26889  atanbndlem  26891  atans2  26897  leibpi  26908  log2tlbnd  26911  birthdaylem3  26919  efrlim  26935  efrlimOLD  26936  jensenlem2  26954  zetacvg  26981  ftalem1  27039  ftalem5  27043  basellem1  27047  basellem4  27050  fsumdvdsdiaglem  27149  dvdsflf1o  27153  fsumfldivdiaglem  27155  ppiub  27171  mersenne  27194  dchrptlem1  27231  bposlem1  27251  bposlem2  27252  bposlem4  27254  lgsdilem  27291  lgseisenlem1  27342  lgseisenlem2  27343  lgseisenlem3  27344  lgsquadlem1  27347  lgsquadlem2  27348  2sqlem3  27387  2sqlem8  27393  2sqlem11  27396  2sqblem  27398  chebbnd1lem2  27437  chebbnd1lem3  27438  rplogsumlem1  27451  rplogsumlem2  27452  dchrisumlem1  27456  dchrmusum2  27461  dchrisum0flblem1  27475  mulog2sumlem1  27501  logdivbnd  27523  pntpbnd1a  27552  pntpbnd1  27553  pntpbnd2  27554  pntlemh  27566  pntlemr  27569  pntlemk  27573  pntlemo  27574  ostth2lem1  27585  ostth2lem2  27601  ostth2lem3  27602  ostth3  27605  noextenddif  27636  noextendlt  27637  noextendgt  27638  nosupbnd1lem3  27678  nosupbnd1lem4  27679  nosupbnd1lem5  27680  nosupbnd1lem6  27681  noinfbnd1lem3  27693  noinfbnd1lem4  27694  noinfbnd1lem5  27695  noinfbnd1lem6  27696  noetasuplem4  27704  madecut  27879  cofcut2  27918  eucliddivs  28372  legov  28657  axsegcon  29000  axpaschlem  29013  0uhgrsubgr  29352  clwwlkf1  30124  upgr4cycl4dv4e  30260  eupth2lem3lem3  30305  nrt2irr  30548  nmblolbii  30874  nmbdoplbi  32099  nmcoplbi  32103  nmophmi  32106  nmbdfnlbi  32124  nmcfnlbi  32127  cnlnadjlem7  32148  nmopcoi  32170  resf1o  32809  muldivdid  32820  receqid  32824  xdivrec  33008  cycpmfvlem  33194  cycpmfv3  33197  lbsdiflsp0  33783  txomap  33991  unitdivcld  34058  measvunilem  34369  measvuni  34371  measssd  34372  measiuns  34374  measinblem  34377  measdivcst  34381  sibfof  34497  oddpwdc  34511  sseqfv1  34546  sseqfv2  34551  probun  34576  totprobd  34583  dstrvprob  34629  actfunsnrndisj  34762  reprsuc  34772  breprexplema  34787  subfaclim  35382  connpconn  35429  cvmliftlem2  35480  cvmliftlem6  35484  cvmliftlem7  35485  cvmliftlem8  35486  cvmliftlem9  35487  cvmliftlem10  35488  snmlff  35523  lineext  36270  hilbert1.1  36348  nn0prpwlem  36516  poimirlem1  37818  opnmbllem0  37853  ismblfin  37858  itgabsnc  37886  ftc1cnnclem  37888  bfplem1  38019  bfp  38021  lfl1  39326  lfladdcl  39327  eqlkr  39355  lkrlsp  39358  atcvrj2b  39688  3dim1  39723  3dim2  39724  llni2  39768  2llnjaN  39822  lvoli3  39833  lvoli2  39837  lncvrelatN  40037  lhpat4N  40300  lhpat3  40302  4atexlemex6  40330  ldilco  40372  ltrnid  40391  ltrnatb  40393  ltrnel  40395  ltrncnvel  40398  ltrncnv  40402  ltrn11at  40403  ltrneq  40405  trlat  40425  trlator0  40427  ltrnnidn  40430  trlid0  40432  trlnidatb  40433  trlnle  40442  trlval3  40443  trlval4  40444  cdlemc2  40448  cdlemc5  40451  cdlemc6  40452  cdlemc  40453  cdlemd2  40455  cdlemd9  40462  cdleme0e  40473  cdleme02N  40478  cdleme0ex1N  40479  cdleme3e  40488  cdleme3g  40490  cdleme3h  40491  cdleme3  40493  cdleme7aa  40498  cdleme7b  40500  cdleme7c  40501  cdleme7d  40502  cdleme7e  40503  cdleme7ga  40504  cdleme7  40505  cdleme9  40509  cdleme16aN  40515  cdleme11c  40517  cdleme11dN  40518  cdleme11e  40519  cdleme11h  40522  cdleme11j  40523  cdleme11k  40524  cdleme12  40527  cdleme21j  40592  cdleme26eALTN  40617  cdleme26f  40619  cdleme26f2  40621  cdlemefrs29bpre0  40652  cdleme35a  40704  cdleme35b  40706  cdleme35c  40707  cdleme35f  40710  cdleme36a  40716  cdleme38m  40719  cdlemeg46rgv  40784  cdlemeg46req  40785  cdlemf  40819  cdlemg2fvlem  40850  cdlemg2l  40859  cdlemg7N  40882  cdlemg12g  40905  cdlemg15  40912  cdlemg17h  40924  cdlemg17  40933  cdlemg19a  40939  cdlemg24  40944  cdlemg37  40945  cdlemg27a  40948  cdlemg31b0N  40950  cdlemg27b  40952  cdlemg31c  40955  cdlemg31d  40956  cdlemg35  40969  trljco  40996  tgrpgrplem  41005  cdlemh2  41072  tendoconid  41085  tendotr  41086  cdlemk35s-id  41194  cdlemk39s-id  41196  cdlemk53b  41212  cdlemk53  41213  cdlemk54  41214  cdleml3N  41234  cdleml5N  41236  tendospcanN  41279  diclss  41449  dihvalcq2  41503  dihord4  41514  dihord5b  41515  dihord5apre  41518  dihmeetlem1N  41546  dihmeetbclemN  41560  dihmeetlem20N  41582  dihmeetALTN  41583  dihatlat  41590  dihatexv  41594  dochkr1  41734  dochkr1OLDN  41735  lcfl7lem  41755  lclkrlem2m  41775  hdmaplna1  42163  hdmaplns1  42164  hdmaplnm1  42165  cxp111d  42593  eldioph2lem1  42998  fphpdo  43055  irrapxlem1  43060  irrapxlem2  43061  irrapxlem3  43062  irrapxlem5  43064  pellexlem2  43068  pell1234qrreccl  43092  pell1234qrmulcl  43093  pell1234qrdich  43099  pell1qr1  43109  pellqrexplicit  43115  pellfundex  43124  reglogltb  43129  reglogleb  43130  pellfund14  43136  rmxycomplete  43155  jm2.24nn  43197  jm2.17b  43199  jm2.17c  43200  jm2.18  43226  jm2.19lem2  43228  jm2.20nn  43235  jm2.16nn0  43242  jm3.1lem2  43256  areaquad  43454  clsk3nimkb  44277  lemuldiv3d  44407  lemuldiv4d  44408  stoweidlem1  46241  stoweidlem11  46251  stoweidlem14  46254  stoweidlem26  46266  stoweidlem34  46274  stoweidlem38  46278  stoweidlem60  46300  fourierdlem52  46398  etransclem38  46512  2tceilhalfelfzo1  47574  reuopreuprim  47768  quad1  47862  requad1  47864  requad2  47865  isubgr3stgrlem1  48208  isubgr3stgrlem3  48210  gpg3kgrtriexlem1  48325  gpg3kgrtriexlem5  48329  domnmsuppn0  48611  lincvalpr  48660  ldepspr  48715  islindeps2  48725  fldivexpfllog2  48807  eenglngeehlnmlem1  48979  eenglngeehlnmlem2  48980  rrx2linest  48984  prsthinc  49705