MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  con4i 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
Assertion
Ref Expression
con4i

Proof of Theorem con4i
StepHypRef Expression
1 notnot1 122 . 2
2 con4i.1 . 2
31, 2nsyl2 127 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4
This theorem is referenced by:  pm2.21i  131  mt4  137  modal-b  1863  ax6fromc10  2227  axc711to11  2247  axc5c711to11  2251  necon2aiOLD  2693  elimasni  5369  ndmfvrcl  5896  brabv  6342  oprssdm  6456  ndmovrcl  6461  omelon2  6712  omopthi  7325  fsuppres  7874  sdomsdomcardi  8373  alephgeom  8484  pwcdadom  8617  rankcf  9176  adderpq  9355  mulerpq  9356  ltadd2iOLD  9737  ssnn0fi  12094  sadcp1  14105  setcepi  15415  oduclatb  15774  cntzrcl  16365  pmtrfrn  16483  dprddomcld  17032  dprdsubg  17071  psrbagsn  18160  dsmmbas2  18768  dsmmfi  18769  istps  19437  bwthOLD  19911  isusp  20764  dscmet  21093  dscopn  21094  i1f1lem  22096  sqff1o  23456  umgrafi  24322  usgraedgrnv  24377  nbgranself2  24436  wwlknndef  24737  clwwlknndef  24773  dmadjrnb  26825  axpowprim  29076  opelco3  29208  sltintdifex  29423  pw2f1ocnv  30979  kelac1  31009  axc5c4c711toc5  31309  axc5c4c711to11  31312  afvvdm  32226  afvvfunressn  32228  afvvv  32230  afvfv0bi  32237
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
  Copyright terms: Public domain W3C validator