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

Theorem con4i 124
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 116 . 2  |-  ( ps 
->  -.  -.  ps )
2 con4i.1 . 2  |-  ( -. 
ph  ->  -.  ps )
31, 2nsyl2 121 1  |-  ( ps 
->  ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  pm2.21i  125  mt4  131  modal-b  1764  ax10lem2OLD  1992  ax9from9o  2206  ax67to7  2226  ax467to7  2230  necon2ai  2620  omelon2  4824  elimasni  5198  ndmfvrcl  5723  brabv  6087  oprssdm  6195  ndmovrcl  6200  omopthi  6867  sdomsdomcardi  7822  alephgeom  7927  pwcdadom  8060  rankcf  8616  adderpq  8797  mulerpq  8798  ltadd2i  9168  sadcp1  12930  setcepi  14206  oduclatb  14534  cntzrcl  15089  mplrcl  16513  psrbagsn  16518  strov2rcl  16594  istps  16964  isusp  18252  dscmet  18581  dscopn  18582  i1f1lem  19542  sqff1o  20926  umgrafi  21318  usgraedgrnv  21358  nbgranself2  21409  dmadjrnb  23370  axpowprim  25114  sltintdifex  25539  pw2f1ocnv  27006  kelac1  27037  dsmmbas2  27079  dsmmfi  27080  uvcff  27116  pmtrfrn  27276  ax4567to4  27478  ax4567to7  27481  afvvdm  27880  afvvfunressn  27882  afvvv  27884  afvfv0bi  27891
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator