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  3846  2nreu  4397  fveqf1o  7243  frrlem12  8237  enfixsn  9010  gruina  10731  grur1  10733  enqeq  10847  recrec  11839  rec11r  11841  divdivdiv  11843  dmdcan  11852  ddcan  11856  rereccl  11860  div2neg  11865  divmuld  11940  divmul2d  11951  divmul3d  11952  divassd  11953  div12d  11954  div23d  11955  divdird  11956  divsubdird  11957  div11d  11958  ltmul12a  11998  ltdiv1  12007  ltrec  12025  lt2msq1  12027  lediv2  12033  supmul1  12112  qbtwnre  13119  xlemul1a  13208  xlemul1  13210  xadd4d  13223  quoremz  13777  quoremnn0ALT  13779  expgt1  14025  nnlesq  14130  expnbnd  14157  expmulnbnd  14160  discr1  14164  facubnd  14225  pfxsuffeqwrdeq  14622  01sqrexlem6  15172  mulcn2  15521  geomulcvg  15801  cvgrat  15808  eftlub  16036  eflegeo  16048  tanhlt1  16087  sin01bnd  16112  cos01bnd  16113  eirrlem  16131  bitsmod  16365  mulgcd  16477  mulgcddvds  16584  prmind2  16614  qnumgt0  16679  pcpremul  16773  fldivp1  16827  pcfaclem  16828  qexpz  16831  prmpwdvds  16834  pockthg  16836  prmreclem1  16846  prmreclem5  16850  4sqlem10  16877  4sqlem12  16886  4sqlem16  16890  4sqlem17  16891  vdwlem3  16913  vdwlem8  16918  vdwlem9  16919  0ram  16950  ramz2  16954  cat1lem  18021  odmulg  19453  dfod2  19461  odf1o1  19469  odf1o2  19470  sylow3lem4  19527  ablsub4  19707  odadd1  19745  odadd2  19746  ablfacrp2  19966  ablfac1b  19969  ablfac1eu  19972  pgpfac1lem3a  19975  pgpfaclem2  19981  ablsimpgfindlem1  20006  chrcong  21452  znrrg  21490  cygznlem1  21491  chpdmatlem3  22743  txdis  23535  txdis1cn  23538  ptunhmeo  23711  qustgplem  24024  blcld  24409  nlmvscnlem2  24589  blcvx  24702  metds0  24755  metdseq0  24759  icopnfcnv  24856  lebnumii  24881  ipcau2  25150  tcphcphlem1  25151  ipcnlem2  25160  csbren  25315  trirn  25316  dyadf  25508  dyadovol  25510  dyaddisjlem  25512  dyadmaxlem  25514  opnmbllem  25518  mbfmulc2lem  25564  mbfi1fseqlem4  25635  mbfi1fseqlem5  25636  mbfi1fseqlem6  25637  itg2mulclem  25663  itg2monolem1  25667  itg2monolem3  25669  itg2cnlem2  25679  itgabs  25752  dvlip  25914  dvlt0  25926  dvcvx  25941  ftc1lem4  25962  dgrcolem2  26196  aaliou3lem2  26267  aaliou3lem9  26274  itgulm  26333  radcnvlem1  26338  abelthlem2  26358  abelthlem7  26364  tangtx  26430  cosne0  26454  cosordlem  26455  tanord1  26462  logdivlti  26545  logcnlem4  26570  logf1o2  26575  cxpcn3lem  26673  cxpaddle  26678  ang180lem2  26736  atanlogsublem  26841  atantan  26849  atanbndlem  26851  atans2  26857  leibpi  26868  log2tlbnd  26871  birthdaylem3  26879  efrlim  26895  efrlimOLD  26896  jensenlem2  26914  zetacvg  26941  ftalem1  26999  ftalem5  27003  basellem1  27007  basellem4  27010  fsumdvdsdiaglem  27109  dvdsflf1o  27113  fsumfldivdiaglem  27115  ppiub  27131  mersenne  27154  dchrptlem1  27191  bposlem1  27211  bposlem2  27212  bposlem4  27214  lgsdilem  27251  lgseisenlem1  27302  lgseisenlem2  27303  lgseisenlem3  27304  lgsquadlem1  27307  lgsquadlem2  27308  2sqlem3  27347  2sqlem8  27353  2sqlem11  27356  2sqblem  27358  chebbnd1lem2  27397  chebbnd1lem3  27398  rplogsumlem1  27411  rplogsumlem2  27412  dchrisumlem1  27416  dchrmusum2  27421  dchrisum0flblem1  27435  mulog2sumlem1  27461  logdivbnd  27483  pntpbnd1a  27512  pntpbnd1  27513  pntpbnd2  27514  pntlemh  27526  pntlemr  27529  pntlemk  27533  pntlemo  27534  ostth2lem1  27545  ostth2lem2  27561  ostth2lem3  27562  ostth3  27565  noextenddif  27596  noextendlt  27597  noextendgt  27598  nosupbnd1lem3  27638  nosupbnd1lem4  27639  nosupbnd1lem5  27640  nosupbnd1lem6  27641  noinfbnd1lem3  27653  noinfbnd1lem4  27654  noinfbnd1lem5  27655  noinfbnd1lem6  27656  noetasuplem4  27664  madecut  27815  cofcut2  27853  eucliddivs  28288  legov  28548  axsegcon  28890  axpaschlem  28903  0uhgrsubgr  29242  clwwlkf1  30011  upgr4cycl4dv4e  30147  eupth2lem3lem3  30192  nrt2irr  30435  nmblolbii  30761  nmbdoplbi  31986  nmcoplbi  31990  nmophmi  31993  nmbdfnlbi  32011  nmcfnlbi  32014  cnlnadjlem7  32035  nmopcoi  32057  resf1o  32686  muldivdid  32697  receqid  32701  xdivrec  32880  cycpmfvlem  33067  cycpmfv3  33070  lbsdiflsp0  33598  txomap  33800  unitdivcld  33867  measvunilem  34178  measvuni  34180  measssd  34181  measiuns  34183  measinblem  34186  measdivcst  34190  sibfof  34307  oddpwdc  34321  sseqfv1  34356  sseqfv2  34361  probun  34386  totprobd  34393  dstrvprob  34439  actfunsnrndisj  34572  reprsuc  34582  breprexplema  34597  subfaclim  35160  connpconn  35207  cvmliftlem2  35258  cvmliftlem6  35262  cvmliftlem7  35263  cvmliftlem8  35264  cvmliftlem9  35265  cvmliftlem10  35266  snmlff  35301  lineext  36049  hilbert1.1  36127  nn0prpwlem  36295  poimirlem1  37600  opnmbllem0  37635  ismblfin  37640  itgabsnc  37668  ftc1cnnclem  37670  bfplem1  37801  bfp  37803  lfl1  39048  lfladdcl  39049  eqlkr  39077  lkrlsp  39080  atcvrj2b  39411  3dim1  39446  3dim2  39447  llni2  39491  2llnjaN  39545  lvoli3  39556  lvoli2  39560  lncvrelatN  39760  lhpat4N  40023  lhpat3  40025  4atexlemex6  40053  ldilco  40095  ltrnid  40114  ltrnatb  40116  ltrnel  40118  ltrncnvel  40121  ltrncnv  40125  ltrn11at  40126  ltrneq  40128  trlat  40148  trlator0  40150  ltrnnidn  40153  trlid0  40155  trlnidatb  40156  trlnle  40165  trlval3  40166  trlval4  40167  cdlemc2  40171  cdlemc5  40174  cdlemc6  40175  cdlemc  40176  cdlemd2  40178  cdlemd9  40185  cdleme0e  40196  cdleme02N  40201  cdleme0ex1N  40202  cdleme3e  40211  cdleme3g  40213  cdleme3h  40214  cdleme3  40216  cdleme7aa  40221  cdleme7b  40223  cdleme7c  40224  cdleme7d  40225  cdleme7e  40226  cdleme7ga  40227  cdleme7  40228  cdleme9  40232  cdleme16aN  40238  cdleme11c  40240  cdleme11dN  40241  cdleme11e  40242  cdleme11h  40245  cdleme11j  40246  cdleme11k  40247  cdleme12  40250  cdleme21j  40315  cdleme26eALTN  40340  cdleme26f  40342  cdleme26f2  40344  cdlemefrs29bpre0  40375  cdleme35a  40427  cdleme35b  40429  cdleme35c  40430  cdleme35f  40433  cdleme36a  40439  cdleme38m  40442  cdlemeg46rgv  40507  cdlemeg46req  40508  cdlemf  40542  cdlemg2fvlem  40573  cdlemg2l  40582  cdlemg7N  40605  cdlemg12g  40628  cdlemg15  40635  cdlemg17h  40647  cdlemg17  40656  cdlemg19a  40662  cdlemg24  40667  cdlemg37  40668  cdlemg27a  40671  cdlemg31b0N  40673  cdlemg27b  40675  cdlemg31c  40678  cdlemg31d  40679  cdlemg35  40692  trljco  40719  tgrpgrplem  40728  cdlemh2  40795  tendoconid  40808  tendotr  40809  cdlemk35s-id  40917  cdlemk39s-id  40919  cdlemk53b  40935  cdlemk53  40936  cdlemk54  40937  cdleml3N  40957  cdleml5N  40959  tendospcanN  41002  diclss  41172  dihvalcq2  41226  dihord4  41237  dihord5b  41238  dihord5apre  41241  dihmeetlem1N  41269  dihmeetbclemN  41283  dihmeetlem20N  41305  dihmeetALTN  41306  dihatlat  41313  dihatexv  41317  dochkr1  41457  dochkr1OLDN  41458  lcfl7lem  41478  lclkrlem2m  41498  hdmaplna1  41886  hdmaplns1  41887  hdmaplnm1  41888  cxp111d  42315  eldioph2lem1  42733  fphpdo  42790  irrapxlem1  42795  irrapxlem2  42796  irrapxlem3  42797  irrapxlem5  42799  pellexlem2  42803  pell1234qrreccl  42827  pell1234qrmulcl  42828  pell1234qrdich  42834  pell1qr1  42844  pellqrexplicit  42850  pellfundex  42859  reglogltb  42864  reglogleb  42865  pellfund14  42871  rmxycomplete  42890  jm2.24nn  42932  jm2.17b  42934  jm2.17c  42935  jm2.18  42961  jm2.19lem2  42963  jm2.20nn  42970  jm2.16nn0  42977  jm3.1lem2  42991  areaquad  43189  clsk3nimkb  44013  lemuldiv3d  44143  lemuldiv4d  44144  stoweidlem1  45983  stoweidlem11  45993  stoweidlem14  45996  stoweidlem26  46008  stoweidlem34  46016  stoweidlem38  46020  stoweidlem60  46042  fourierdlem52  46140  etransclem38  46254  2tceilhalfelfzo1  47317  reuopreuprim  47511  quad1  47605  requad1  47607  requad2  47608  isubgr3stgrlem1  47951  isubgr3stgrlem3  47953  gpg3kgrtriexlem1  48068  gpg3kgrtriexlem5  48072  domnmsuppn0  48354  lincvalpr  48404  ldepspr  48459  islindeps2  48469  fldivexpfllog2  48551  eenglngeehlnmlem1  48723  eenglngeehlnmlem2  48724  rrx2linest  48728  prsthinc  49450