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  1753  ax10lem2  1942  ax9from9o  2153  ax67to7  2173  ax467to7  2177  necon2ai  2566  omelon2  4750  elimasni  5122  ndmfvrcl  5636  oprssdm  6089  ndmovrcl  6093  omopthi  6742  sdomsdomcardi  7694  alephgeom  7799  pwcdadom  7932  rankcf  8489  adderpq  8670  mulerpq  8671  ltadd2i  9040  sadcp1  12743  setcepi  14019  oduclatb  14347  cntzrcl  14902  mplrcl  16330  psrbagsn  16335  strov2rcl  16414  istps  16780  dscmet  18197  dscopn  18198  i1f1lem  19148  sqff1o  20532  dmadjrnb  22600  isusp  23560  umgrafi  24278  axpowprim  24454  sltintdifex  24875  pw2f1ocnv  26453  kelac1  26484  dsmmbas2  26526  dsmmfi  26527  uvcff  26563  pmtrfrn  26723  ax4567to4  26925  ax4567to7  26928  afvvdm  27329  afvvfunressn  27331  afvvv  27333  afvfv0bi  27340  brabv  27433  usgraedgrnv  27552  nbgranself2  27602  ax9lem15  29223
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator