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  3843  2nreu  4394  fveqf1o  7236  frrlem12  8227  enfixsn  8999  gruina  10706  grur1  10708  enqeq  10822  recrec  11815  rec11r  11817  divdivdiv  11819  dmdcan  11828  ddcan  11832  rereccl  11836  div2neg  11841  divmuld  11916  divmul2d  11927  divmul3d  11928  divassd  11929  div12d  11930  div23d  11931  divdird  11932  divsubdird  11933  div11d  11934  ltmul12a  11974  ltdiv1  11983  ltrec  12001  lt2msq1  12003  lediv2  12009  supmul1  12088  qbtwnre  13095  xlemul1a  13184  xlemul1  13186  xadd4d  13199  quoremz  13756  quoremnn0ALT  13758  expgt1  14004  nnlesq  14109  expnbnd  14136  expmulnbnd  14139  discr1  14143  facubnd  14204  pfxsuffeqwrdeq  14602  01sqrexlem6  15151  mulcn2  15500  geomulcvg  15780  cvgrat  15787  eftlub  16015  eflegeo  16027  tanhlt1  16066  sin01bnd  16091  cos01bnd  16092  eirrlem  16110  bitsmod  16344  mulgcd  16456  mulgcddvds  16563  prmind2  16593  qnumgt0  16658  pcpremul  16752  fldivp1  16806  pcfaclem  16807  qexpz  16810  prmpwdvds  16813  pockthg  16815  prmreclem1  16825  prmreclem5  16829  4sqlem10  16856  4sqlem12  16865  4sqlem16  16869  4sqlem17  16870  vdwlem3  16892  vdwlem8  16897  vdwlem9  16898  0ram  16929  ramz2  16933  cat1lem  18000  odmulg  19466  dfod2  19474  odf1o1  19482  odf1o2  19483  sylow3lem4  19540  ablsub4  19720  odadd1  19758  odadd2  19759  ablfacrp2  19979  ablfac1b  19982  ablfac1eu  19985  pgpfac1lem3a  19988  pgpfaclem2  19994  ablsimpgfindlem1  20019  chrcong  21462  znrrg  21500  cygznlem1  21501  chpdmatlem3  22753  txdis  23545  txdis1cn  23548  ptunhmeo  23721  qustgplem  24034  blcld  24418  nlmvscnlem2  24598  blcvx  24711  metds0  24764  metdseq0  24768  icopnfcnv  24865  lebnumii  24890  ipcau2  25159  tcphcphlem1  25160  ipcnlem2  25169  csbren  25324  trirn  25325  dyadf  25517  dyadovol  25519  dyaddisjlem  25521  dyadmaxlem  25523  opnmbllem  25527  mbfmulc2lem  25573  mbfi1fseqlem4  25644  mbfi1fseqlem5  25645  mbfi1fseqlem6  25646  itg2mulclem  25672  itg2monolem1  25676  itg2monolem3  25678  itg2cnlem2  25688  itgabs  25761  dvlip  25923  dvlt0  25935  dvcvx  25950  ftc1lem4  25971  dgrcolem2  26205  aaliou3lem2  26276  aaliou3lem9  26283  itgulm  26342  radcnvlem1  26347  abelthlem2  26367  abelthlem7  26373  tangtx  26439  cosne0  26463  cosordlem  26464  tanord1  26471  logdivlti  26554  logcnlem4  26579  logf1o2  26584  cxpcn3lem  26682  cxpaddle  26687  ang180lem2  26745  atanlogsublem  26850  atantan  26858  atanbndlem  26860  atans2  26866  leibpi  26877  log2tlbnd  26880  birthdaylem3  26888  efrlim  26904  efrlimOLD  26905  jensenlem2  26923  zetacvg  26950  ftalem1  27008  ftalem5  27012  basellem1  27016  basellem4  27019  fsumdvdsdiaglem  27118  dvdsflf1o  27122  fsumfldivdiaglem  27124  ppiub  27140  mersenne  27163  dchrptlem1  27200  bposlem1  27220  bposlem2  27221  bposlem4  27223  lgsdilem  27260  lgseisenlem1  27311  lgseisenlem2  27312  lgseisenlem3  27313  lgsquadlem1  27316  lgsquadlem2  27317  2sqlem3  27356  2sqlem8  27362  2sqlem11  27365  2sqblem  27367  chebbnd1lem2  27406  chebbnd1lem3  27407  rplogsumlem1  27420  rplogsumlem2  27421  dchrisumlem1  27425  dchrmusum2  27430  dchrisum0flblem1  27444  mulog2sumlem1  27470  logdivbnd  27492  pntpbnd1a  27521  pntpbnd1  27522  pntpbnd2  27523  pntlemh  27535  pntlemr  27538  pntlemk  27542  pntlemo  27543  ostth2lem1  27554  ostth2lem2  27570  ostth2lem3  27571  ostth3  27574  noextenddif  27605  noextendlt  27606  noextendgt  27607  nosupbnd1lem3  27647  nosupbnd1lem4  27648  nosupbnd1lem5  27649  nosupbnd1lem6  27650  noinfbnd1lem3  27662  noinfbnd1lem4  27663  noinfbnd1lem5  27664  noinfbnd1lem6  27665  noetasuplem4  27673  madecut  27826  cofcut2  27864  eucliddivs  28299  legov  28561  axsegcon  28903  axpaschlem  28916  0uhgrsubgr  29255  clwwlkf1  30024  upgr4cycl4dv4e  30160  eupth2lem3lem3  30205  nrt2irr  30448  nmblolbii  30774  nmbdoplbi  31999  nmcoplbi  32003  nmophmi  32006  nmbdfnlbi  32024  nmcfnlbi  32027  cnlnadjlem7  32048  nmopcoi  32070  resf1o  32708  muldivdid  32719  receqid  32723  xdivrec  32902  cycpmfvlem  33076  cycpmfv3  33079  lbsdiflsp0  33634  txomap  33842  unitdivcld  33909  measvunilem  34220  measvuni  34222  measssd  34223  measiuns  34225  measinblem  34228  measdivcst  34232  sibfof  34348  oddpwdc  34362  sseqfv1  34397  sseqfv2  34402  probun  34427  totprobd  34434  dstrvprob  34480  actfunsnrndisj  34613  reprsuc  34623  breprexplema  34638  subfaclim  35220  connpconn  35267  cvmliftlem2  35318  cvmliftlem6  35322  cvmliftlem7  35323  cvmliftlem8  35324  cvmliftlem9  35325  cvmliftlem10  35326  snmlff  35361  lineext  36109  hilbert1.1  36187  nn0prpwlem  36355  poimirlem1  37660  opnmbllem0  37695  ismblfin  37700  itgabsnc  37728  ftc1cnnclem  37730  bfplem1  37861  bfp  37863  lfl1  39108  lfladdcl  39109  eqlkr  39137  lkrlsp  39140  atcvrj2b  39470  3dim1  39505  3dim2  39506  llni2  39550  2llnjaN  39604  lvoli3  39615  lvoli2  39619  lncvrelatN  39819  lhpat4N  40082  lhpat3  40084  4atexlemex6  40112  ldilco  40154  ltrnid  40173  ltrnatb  40175  ltrnel  40177  ltrncnvel  40180  ltrncnv  40184  ltrn11at  40185  ltrneq  40187  trlat  40207  trlator0  40209  ltrnnidn  40212  trlid0  40214  trlnidatb  40215  trlnle  40224  trlval3  40225  trlval4  40226  cdlemc2  40230  cdlemc5  40233  cdlemc6  40234  cdlemc  40235  cdlemd2  40237  cdlemd9  40244  cdleme0e  40255  cdleme02N  40260  cdleme0ex1N  40261  cdleme3e  40270  cdleme3g  40272  cdleme3h  40273  cdleme3  40275  cdleme7aa  40280  cdleme7b  40282  cdleme7c  40283  cdleme7d  40284  cdleme7e  40285  cdleme7ga  40286  cdleme7  40287  cdleme9  40291  cdleme16aN  40297  cdleme11c  40299  cdleme11dN  40300  cdleme11e  40301  cdleme11h  40304  cdleme11j  40305  cdleme11k  40306  cdleme12  40309  cdleme21j  40374  cdleme26eALTN  40399  cdleme26f  40401  cdleme26f2  40403  cdlemefrs29bpre0  40434  cdleme35a  40486  cdleme35b  40488  cdleme35c  40489  cdleme35f  40492  cdleme36a  40498  cdleme38m  40501  cdlemeg46rgv  40566  cdlemeg46req  40567  cdlemf  40601  cdlemg2fvlem  40632  cdlemg2l  40641  cdlemg7N  40664  cdlemg12g  40687  cdlemg15  40694  cdlemg17h  40706  cdlemg17  40715  cdlemg19a  40721  cdlemg24  40726  cdlemg37  40727  cdlemg27a  40730  cdlemg31b0N  40732  cdlemg27b  40734  cdlemg31c  40737  cdlemg31d  40738  cdlemg35  40751  trljco  40778  tgrpgrplem  40787  cdlemh2  40854  tendoconid  40867  tendotr  40868  cdlemk35s-id  40976  cdlemk39s-id  40978  cdlemk53b  40994  cdlemk53  40995  cdlemk54  40996  cdleml3N  41016  cdleml5N  41018  tendospcanN  41061  diclss  41231  dihvalcq2  41285  dihord4  41296  dihord5b  41297  dihord5apre  41300  dihmeetlem1N  41328  dihmeetbclemN  41342  dihmeetlem20N  41364  dihmeetALTN  41365  dihatlat  41372  dihatexv  41376  dochkr1  41516  dochkr1OLDN  41517  lcfl7lem  41537  lclkrlem2m  41557  hdmaplna1  41945  hdmaplns1  41946  hdmaplnm1  41947  cxp111d  42374  eldioph2lem1  42792  fphpdo  42849  irrapxlem1  42854  irrapxlem2  42855  irrapxlem3  42856  irrapxlem5  42858  pellexlem2  42862  pell1234qrreccl  42886  pell1234qrmulcl  42887  pell1234qrdich  42893  pell1qr1  42903  pellqrexplicit  42909  pellfundex  42918  reglogltb  42923  reglogleb  42924  pellfund14  42930  rmxycomplete  42949  jm2.24nn  42991  jm2.17b  42993  jm2.17c  42994  jm2.18  43020  jm2.19lem2  43022  jm2.20nn  43029  jm2.16nn0  43036  jm3.1lem2  43050  areaquad  43248  clsk3nimkb  44072  lemuldiv3d  44202  lemuldiv4d  44203  stoweidlem1  46038  stoweidlem11  46048  stoweidlem14  46051  stoweidlem26  46063  stoweidlem34  46071  stoweidlem38  46075  stoweidlem60  46097  fourierdlem52  46195  etransclem38  46309  2tceilhalfelfzo1  47362  reuopreuprim  47556  quad1  47650  requad1  47652  requad2  47653  isubgr3stgrlem1  47996  isubgr3stgrlem3  47998  gpg3kgrtriexlem1  48113  gpg3kgrtriexlem5  48117  domnmsuppn0  48399  lincvalpr  48449  ldepspr  48504  islindeps2  48514  fldivexpfllog2  48596  eenglngeehlnmlem1  48768  eenglngeehlnmlem2  48769  rrx2linest  48773  prsthinc  49495