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

Theorem con4i 122
Description: Inference rule derived from axiom ax-3 7. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 21-Jun-2013.)
Hypothesis
Ref Expression
con4i.1  |-  ( -. 
ph  ->  -.  ps )
Assertion
Ref Expression
con4i  |-  ( ps 
->  ph )

Proof of Theorem con4i
StepHypRef Expression
1 notnot1 114 . 2  |-  ( ps 
->  -.  -.  ps )
2 con4i.1 . 2  |-  ( -. 
ph  ->  -.  ps )
31, 2nsyl2 119 1  |-  ( ps 
->  ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  pm2.21i  123  mt4  129  modal-b  1779  ax10lem2  1877  ax9from9o  2087  ax67to7  2107  ax467to7  2111  necon2ai  2491  omelon2  4668  elimasni  5040  ndmfvrcl  5553  oprssdm  6002  ndmovrcl  6006  omopthi  6655  sdomsdomcardi  7604  alephgeom  7709  pwcdadom  7842  rankcf  8399  adderpq  8580  mulerpq  8581  ltadd2i  8950  sadcp1  12646  setcepi  13920  oduclatb  14248  cntzrcl  14803  mplrcl  16231  psrbagsn  16236  strov2rcl  16315  istps  16674  dscmet  18095  dscopn  18096  i1f1lem  19044  sqff1o  20420  dmadjrnb  22486  umgrafi  23874  axpowprim  24050  sltintdifex  24317  evpexun  24998  dstr  25171  bwt2  25592  pw2f1ocnv  27130  kelac1  27161  dsmmbas2  27203  dsmmfi  27204  uvcff  27240  pmtrfrn  27400  ax4567to4  27602  ax4567to7  27605  afvvdm  28004  afvvfunressn  28006  afvvv  28008  afvfv0bi  28015  usgraedgrnv  28123  nbgranself2  28151  ax9lem15  29154
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator