MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl211anc Structured version   Visualization version   GIF version

Theorem syl211anc 1378
Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
Hypotheses
Ref Expression
syl3anc.1 (𝜑𝜓)
syl3anc.2 (𝜑𝜒)
syl3anc.3 (𝜑𝜃)
syl3Xanc.4 (𝜑𝜏)
syl211anc.5 (((𝜓𝜒) ∧ 𝜃𝜏) → 𝜂)
Assertion
Ref Expression
syl211anc (𝜑𝜂)

Proof of Theorem syl211anc
StepHypRef Expression
1 syl3anc.1 . . 3 (𝜑𝜓)
2 syl3anc.2 . . 3 (𝜑𝜒)
31, 2jca 511 . 2 (𝜑 → (𝜓𝜒))
4 syl3anc.3 . 2 (𝜑𝜃)
5 syl3Xanc.4 . 2 (𝜑𝜏)
6 syl211anc.5 . 2 (((𝜓𝜒) ∧ 𝜃𝜏) → 𝜂)
73, 4, 5, 6syl3anc 1373 1 (𝜑𝜂)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  w3a 1087
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 1089
This theorem is referenced by:  syl212anc  1382  syl221anc  1383  frrlem15  9797  supicc  13541  modaddmulmod  13979  limsupgre  15517  limsupbnd1  15518  limsupbnd2  15519  lbspss  21081  lindff1  21840  islinds4  21855  mdetunilem9  22626  madutpos  22648  neiptopnei  23140  mbflimsup  25701  cxpneg  26723  cxpmul2  26731  cxpsqrt  26745  cxpaddd  26759  cxpsubd  26760  divcxpd  26764  fsumharmonic  27055  bposlem1  27328  lgsqr  27395  chpchtlim  27523  sltmul2d  28198  ax5seg  28953  archiabllem2c  33202  qsidomlem2  33481  dimlssid  33683  logdivsqrle  34665  lindsadd  37620  lshpnelb  38985  cdlemg2fv2  40602  cdlemg2m  40606  cdlemg9a  40634  cdlemg9b  40635  cdlemg12b  40646  cdlemg14f  40655  cdlemg14g  40656  cdlemg17dN  40665  cdlemkj  40865  cdlemkuv2  40869  cdlemk52  40956  cdlemk53a  40957  mullimc  45631  mullimcf  45638  sfprmdvdsmersenne  47590  lincfsuppcl  48330
  Copyright terms: Public domain W3C validator