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

Theorem con4i 125
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 117 . 2  |-  ( ps 
->  -.  -.  ps )
2 con4i.1 . 2  |-  ( -. 
ph  ->  -.  ps )
31, 2nsyl2 122 1  |-  ( ps 
->  ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  pm2.21i  126  mt4  132  modal-b  1769  ax10lem2OLD  2027  ax9from9o  2226  ax67to7  2246  ax467to7  2250  necon2ai  2650  omelon2  4858  elimasni  5232  ndmfvrcl  5757  brabv  6121  oprssdm  6229  ndmovrcl  6234  omopthi  6901  sdomsdomcardi  7859  alephgeom  7964  pwcdadom  8097  rankcf  8653  adderpq  8834  mulerpq  8835  ltadd2i  9205  sadcp1  12968  setcepi  14244  oduclatb  14572  cntzrcl  15127  mplrcl  16551  psrbagsn  16556  strov2rcl  16632  istps  17002  bwth  17474  isusp  18292  dscmet  18621  dscopn  18622  i1f1lem  19582  sqff1o  20966  umgrafi  21358  usgraedgrnv  21398  nbgranself2  21449  dmadjrnb  23410  axpowprim  25154  opelco3  25404  sltintdifex  25619  pw2f1ocnv  27109  kelac1  27139  dsmmbas2  27181  dsmmfi  27182  uvcff  27218  pmtrfrn  27378  ax4567to4  27580  ax4567to7  27583  afvvdm  27982  afvvfunressn  27984  afvvv  27986  afvfv0bi  27993
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator