Theorem syl112anc 1373

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 1370	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  3900  2nreu  4449  fveqf1o  7321  frrlem12  8320  enfixsn  9119  gruina  10855  grur1  10857  enqeq  10971  recrec  11961  rec11r  11963  divdivdiv  11965  dmdcan  11974  ddcan  11978  rereccl  11982  div2neg  11987  divmuld  12062  divmul2d  12073  divmul3d  12074  divassd  12075  div12d  12076  div23d  12077  divdird  12078  divsubdird  12079  div11d  12080  ltmul12a  12120  ltdiv1  12129  ltrec  12147  lt2msq1  12149  lediv2  12155  supmul1  12234  qbtwnre  13237  xlemul1a  13326  xlemul1  13328  xadd4d  13341  quoremz  13891  quoremnn0ALT  13893  expgt1  14137  nnlesq  14240  expnbnd  14267  expmulnbnd  14270  discr1  14274  facubnd  14335  pfxsuffeqwrdeq  14732  01sqrexlem6  15282  mulcn2  15628  geomulcvg  15908  cvgrat  15915  eftlub  16141  eflegeo  16153  tanhlt1  16192  sin01bnd  16217  cos01bnd  16218  eirrlem  16236  bitsmod  16469  mulgcd  16581  mulgcddvds  16688  prmind2  16718  qnumgt0  16783  pcpremul  16876  fldivp1  16930  pcfaclem  16931  qexpz  16934  prmpwdvds  16937  pockthg  16939  prmreclem1  16949  prmreclem5  16953  4sqlem10  16980  4sqlem12  16989  4sqlem16  16993  4sqlem17  16994  vdwlem3  17016  vdwlem8  17021  vdwlem9  17022  0ram  17053  ramz2  17057  cat1lem  18149  odmulg  19588  dfod2  19596  odf1o1  19604  odf1o2  19605  sylow3lem4  19662  ablsub4  19842  odadd1  19880  odadd2  19881  ablfacrp2  20101  ablfac1b  20104  ablfac1eu  20107  pgpfac1lem3a  20110  pgpfaclem2  20116  ablsimpgfindlem1  20141  chrcong  21559  znrrg  21601  cygznlem1  21602  chpdmatlem3  22861  txdis  23655  txdis1cn  23658  ptunhmeo  23831  qustgplem  24144  blcld  24533  nlmvscnlem2  24721  blcvx  24833  metds0  24885  metdseq0  24889  icopnfcnv  24986  lebnumii  25011  ipcau2  25281  tcphcphlem1  25282  ipcnlem2  25291  csbren  25446  trirn  25447  dyadf  25639  dyadovol  25641  dyaddisjlem  25643  dyadmaxlem  25645  opnmbllem  25649  mbfmulc2lem  25695  mbfi1fseqlem4  25767  mbfi1fseqlem5  25768  mbfi1fseqlem6  25769  itg2mulclem  25795  itg2monolem1  25799  itg2monolem3  25801  itg2cnlem2  25811  itgabs  25884  dvlip  26046  dvlt0  26058  dvcvx  26073  ftc1lem4  26094  dgrcolem2  26328  aaliou3lem2  26399  aaliou3lem9  26406  itgulm  26465  radcnvlem1  26470  abelthlem2  26490  abelthlem7  26496  tangtx  26561  cosne0  26585  cosordlem  26586  tanord1  26593  logdivlti  26676  logcnlem4  26701  logf1o2  26706  cxpcn3lem  26804  cxpaddle  26809  ang180lem2  26867  atanlogsublem  26972  atantan  26980  atanbndlem  26982  atans2  26988  leibpi  26999  log2tlbnd  27002  birthdaylem3  27010  efrlim  27026  efrlimOLD  27027  jensenlem2  27045  zetacvg  27072  ftalem1  27130  ftalem5  27134  basellem1  27138  basellem4  27141  fsumdvdsdiaglem  27240  dvdsflf1o  27244  fsumfldivdiaglem  27246  ppiub  27262  mersenne  27285  dchrptlem1  27322  bposlem1  27342  bposlem2  27343  bposlem4  27345  lgsdilem  27382  lgseisenlem1  27433  lgseisenlem2  27434  lgseisenlem3  27435  lgsquadlem1  27438  lgsquadlem2  27439  2sqlem3  27478  2sqlem8  27484  2sqlem11  27487  2sqblem  27489  chebbnd1lem2  27528  chebbnd1lem3  27529  rplogsumlem1  27542  rplogsumlem2  27543  dchrisumlem1  27547  dchrmusum2  27552  dchrisum0flblem1  27566  mulog2sumlem1  27592  logdivbnd  27614  pntpbnd1a  27643  pntpbnd1  27644  pntpbnd2  27645  pntlemh  27657  pntlemr  27660  pntlemk  27664  pntlemo  27665  ostth2lem1  27676  ostth2lem2  27692  ostth2lem3  27693  ostth3  27696  noextenddif  27727  noextendlt  27728  noextendgt  27729  nosupbnd1lem3  27769  nosupbnd1lem4  27770  nosupbnd1lem5  27771  nosupbnd1lem6  27772  noinfbnd1lem3  27784  noinfbnd1lem4  27785  noinfbnd1lem5  27786  noinfbnd1lem6  27787  noetasuplem4  27795  madecut  27935  cofcut2  27970  legov  28607  axsegcon  28956  axpaschlem  28969  0uhgrsubgr  29310  clwwlkf1  30077  upgr4cycl4dv4e  30213  eupth2lem3lem3  30258  nrt2irr  30501  nmblolbii  30827  nmbdoplbi  32052  nmcoplbi  32056  nmophmi  32059  nmbdfnlbi  32077  nmcfnlbi  32080  cnlnadjlem7  32101  nmopcoi  32123  resf1o  32747  muldivdid  32757  xdivrec  32893  cycpmfvlem  33114  cycpmfv3  33117  lbsdiflsp0  33653  txomap  33794  unitdivcld  33861  measvunilem  34192  measvuni  34194  measssd  34195  measiuns  34197  measinblem  34200  measdivcst  34204  sibfof  34321  oddpwdc  34335  sseqfv1  34370  sseqfv2  34375  probun  34400  totprobd  34407  dstrvprob  34452  actfunsnrndisj  34598  reprsuc  34608  breprexplema  34623  subfaclim  35172  connpconn  35219  cvmliftlem2  35270  cvmliftlem6  35274  cvmliftlem7  35275  cvmliftlem8  35276  cvmliftlem9  35277  cvmliftlem10  35278  snmlff  35313  lineext  36057  hilbert1.1  36135  nn0prpwlem  36304  poimirlem1  37607  opnmbllem0  37642  ismblfin  37647  itgabsnc  37675  ftc1cnnclem  37677  bfplem1  37808  bfp  37810  lfl1  39051  lfladdcl  39052  eqlkr  39080  lkrlsp  39083  atcvrj2b  39414  3dim1  39449  3dim2  39450  llni2  39494  2llnjaN  39548  lvoli3  39559  lvoli2  39563  lncvrelatN  39763  lhpat4N  40026  lhpat3  40028  4atexlemex6  40056  ldilco  40098  ltrnid  40117  ltrnatb  40119  ltrnel  40121  ltrncnvel  40124  ltrncnv  40128  ltrn11at  40129  ltrneq  40131  trlat  40151  trlator0  40153  ltrnnidn  40156  trlid0  40158  trlnidatb  40159  trlnle  40168  trlval3  40169  trlval4  40170  cdlemc2  40174  cdlemc5  40177  cdlemc6  40178  cdlemc  40179  cdlemd2  40181  cdlemd9  40188  cdleme0e  40199  cdleme02N  40204  cdleme0ex1N  40205  cdleme3e  40214  cdleme3g  40216  cdleme3h  40217  cdleme3  40219  cdleme7aa  40224  cdleme7b  40226  cdleme7c  40227  cdleme7d  40228  cdleme7e  40229  cdleme7ga  40230  cdleme7  40231  cdleme9  40235  cdleme16aN  40241  cdleme11c  40243  cdleme11dN  40244  cdleme11e  40245  cdleme11h  40248  cdleme11j  40249  cdleme11k  40250  cdleme12  40253  cdleme21j  40318  cdleme26eALTN  40343  cdleme26f  40345  cdleme26f2  40347  cdlemefrs29bpre0  40378  cdleme35a  40430  cdleme35b  40432  cdleme35c  40433  cdleme35f  40436  cdleme36a  40442  cdleme38m  40445  cdlemeg46rgv  40510  cdlemeg46req  40511  cdlemf  40545  cdlemg2fvlem  40576  cdlemg2l  40585  cdlemg7N  40608  cdlemg12g  40631  cdlemg15  40638  cdlemg17h  40650  cdlemg17  40659  cdlemg19a  40665  cdlemg24  40670  cdlemg37  40671  cdlemg27a  40674  cdlemg31b0N  40676  cdlemg27b  40678  cdlemg31c  40681  cdlemg31d  40682  cdlemg35  40695  trljco  40722  tgrpgrplem  40731  cdlemh2  40798  tendoconid  40811  tendotr  40812  cdlemk35s-id  40920  cdlemk39s-id  40922  cdlemk53b  40938  cdlemk53  40939  cdlemk54  40940  cdleml3N  40960  cdleml5N  40962  tendospcanN  41005  diclss  41175  dihvalcq2  41229  dihord4  41240  dihord5b  41241  dihord5apre  41244  dihmeetlem1N  41272  dihmeetbclemN  41286  dihmeetlem20N  41308  dihmeetALTN  41309  dihatlat  41316  dihatexv  41320  dochkr1  41460  dochkr1OLDN  41461  lcfl7lem  41481  lclkrlem2m  41501  hdmaplna1  41889  hdmaplns1  41890  hdmaplnm1  41891  cxp111d  42356  eldioph2lem1  42747  fphpdo  42804  irrapxlem1  42809  irrapxlem2  42810  irrapxlem3  42811  irrapxlem5  42813  pellexlem2  42817  pell1234qrreccl  42841  pell1234qrmulcl  42842  pell1234qrdich  42848  pell1qr1  42858  pellqrexplicit  42864  pellfundex  42873  reglogltb  42878  reglogleb  42879  pellfund14  42885  rmxycomplete  42905  jm2.24nn  42947  jm2.17b  42949  jm2.17c  42950  jm2.18  42976  jm2.19lem2  42978  jm2.20nn  42985  jm2.16nn0  42992  jm3.1lem2  43006  areaquad  43204  clsk3nimkb  44029  lemuldiv3d  44159  lemuldiv4d  44160  stoweidlem1  45956  stoweidlem11  45966  stoweidlem14  45969  stoweidlem26  45981  stoweidlem34  45989  stoweidlem38  45993  stoweidlem60  46015  fourierdlem52  46113  etransclem38  46227  reuopreuprim  47450  quad1  47544  requad1  47546  requad2  47547  isubgr3stgrlem1  47868  isubgr3stgrlem3  47870  2tceilhalfelfzo1  47952  domnmsuppn0  48213  lincvalpr  48263  ldepspr  48318  islindeps2  48328  fldivexpfllog2  48414  eenglngeehlnmlem1  48586  eenglngeehlnmlem2  48587  rrx2linest  48591  prsthinc  48854