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

Theorem con4d 100
Description: Deduction derived from axiom ax-3 8. (Contributed by NM, 26-Mar-1995.)
Hypothesis
Ref Expression
con4d.1  |-  ( ph  ->  ( -.  ps  ->  -. 
ch ) )
Assertion
Ref Expression
con4d  |-  ( ph  ->  ( ch  ->  ps ) )

Proof of Theorem con4d
StepHypRef Expression
1 con4d.1 . 2  |-  ( ph  ->  ( -.  ps  ->  -. 
ch ) )
2 ax-3 8 . 2  |-  ( ( -.  ps  ->  -.  ch )  ->  ( ch 
->  ps ) )
31, 2syl 16 1  |-  ( ph  ->  ( ch  ->  ps ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  pm2.21d  101  pm2.18  105  con2d  110  con1d  119  mt4d  133  impcon4bid  198  con4bid  286  exim  1585  spOLD  1767  necon2ad  2659  spc2gv  3048  spc3gv  3050  soisoi  6084  isomin  6093  mpt2xopynvov0g  6501  riotaclbg  6625  boxcutc  7141  sdomel  7290  onsdominel  7292  preleq  7608  cantnfreslem  7667  cflim2  8181  cfslbn  8185  cofsmo  8187  fincssdom  8241  fin23lem25  8242  fin23lem26  8243  fin1a2s  8332  pwfseqlem4  8575  ltapr  8960  suplem2pr  8968  qsqueeze  10825  hashbnd  11662  hashclb  11679  hashgt0elex  11708  hashgt12el  11720  hashgt12el2  11721  pc2dvds  13290  infpnlem1  13316  odcl2  15239  ufilmax  17977  ufileu  17989  filufint  17990  hausflim  18051  flimfnfcls  18098  alexsubALTlem3  18118  alexsubALTlem4  18119  reconnlem2  18896  lebnumlem3  19026  itg1ge0a  19639  itg2seq  19670  m1lgs  21184  usgraidx2v  21450  cusgrafilem3  21528  cusgrafi  21529  usgrcyclnl1  21665  ex-natded5.13-2  21762  wfi  25517  frind  25553  axlowdimlem14  25929  meran1  26196  nn0prpw  26368  heiborlem1  26562  eu2ndop1stv  28068  swrdvalodmlem1  28319  bnj23  29257
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
  Copyright terms: Public domain W3C validator