MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl8 Unicode version

Theorem syl8 70
Description: A syllogism rule of inference. The second premise is used to replace the consequent of the first premise. (Contributed by NM, 1-Aug-1994.) (Proof shortened by Wolf Lammen, 3-Aug-2012.)
Hypotheses
Ref Expression
syl8.1
syl8.2
Assertion
Ref Expression
syl8

Proof of Theorem syl8
StepHypRef Expression
1 syl8.1 . 2
2 syl8.2 . . 3
32a1i 11 . 2
41, 3syl6d 69 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4
This theorem is referenced by:  com45  89  syl8ib  231  imp5a  598  3exp  1195  mopickOLD  2357  suctr  4966  ssorduni  6621  tfindsg  6695  findsg  6727  tz7.49  7129  nneneq  7720  dfac2  8532  qreccl  11231  cmpsub  19900  bwthOLD  19911  fclsopni  20516  wlkdvspthlem  24609  sumdmdlem2  27338  nocvxminlem  29450  idinside  29734  a1i4  30114  prtlem15  30616  prtlem17  30617  rngccatidOLD  32797  ringccatidOLD  32860  ee3bir  33272  ee233  33289  onfrALTlem2  33318  ee223  33420  eel32131  33509  ee33VD  33679
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
  Copyright terms: Public domain W3C validator