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

Theorem con4i 130
Description: Inference rule derived from axiom ax-3 8. Its associated inference is mt4 137. (Contributed by NM, 29-Dec-1992.) (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 122 . 2  |-  ( ps 
->  -.  -.  ps )
2 con4i.1 . 2  |-  ( -. 
ph  ->  -.  ps )
31, 2nsyl2 127 1  |-  ( ps 
->  ph )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem is referenced by:  pm2.21i  131  mt4  137  modal-b  1849  ax6fromc10  2213  axc711to11  2233  axc5c711to11  2237  necon2aiOLD  2679  elimasni  5354  ndmfvrcl  5881  brabv  6327  oprssdm  6441  ndmovrcl  6446  omelon2  6697  omopthi  7308  fsuppres  7856  sdomsdomcardi  8355  alephgeom  8466  pwcdadom  8599  rankcf  9158  adderpq  9337  mulerpq  9338  ltadd2iOLD  9719  ssnn0fi  12073  sadcp1  13982  setcepi  15289  oduclatb  15648  cntzrcl  16239  pmtrfrn  16357  dprddomcld  16906  dprdsubg  16945  psrbagsn  18034  dsmmbas2  18641  dsmmfi  18642  istps  19310  bwthOLD  19784  isusp  20637  dscmet  20966  dscopn  20967  i1f1lem  21969  sqff1o  23328  umgrafi  24194  usgraedgrnv  24249  nbgranself2  24308  wwlknndef  24609  clwwlknndef  24645  dmadjrnb  26697  axpowprim  28949  opelco3  29183  sltintdifex  29398  pw2f1ocnv  30954  kelac1  30984  axc5c4c711toc5  31263  axc5c4c711to11  31266  afvvdm  32064  afvvfunressn  32066  afvvv  32068  afvfv0bi  32075
  Copyright terms: Public domain W3C validator