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

Theorem con4d 108
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 17 1  |-  ( ph  ->  ( ch  ->  ps ) )
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.21d  109  pm2.18  113  con2d  118  con1d  127  mt4d  143  impcon4bid  208  con4bid  294  aleximi  1700  necon2adOLD  2638  spc2gv  3169  spc3gv  3171  wfi  5428  soisoi  6230  isomin  6239  riotaclb  6300  extmptsuppeq  6946  mpt2xopynvov0g  6964  boxcutc  7569  sdomel  7721  onsdominel  7723  preleq  8124  cflim2  8693  cfslbn  8697  cofsmo  8699  fincssdom  8753  fin23lem25  8754  fin23lem26  8755  fin1a2s  8844  pwfseqlem4  9087  ltapr  9470  suplem2pr  9478  qsqueeze  11494  ssfzoulel  12004  ssnn0fi  12196  hashbnd  12520  hashclb  12539  hashgt0elex  12577  hashgt12el  12592  hashgt12el2  12593  pc2dvds  14815  infpnlem1  14841  odcl2  17203  ufilmax  20908  ufileu  20920  filufint  20921  hausflim  20982  flimfnfcls  21029  alexsubALTlem3  21050  alexsubALTlem4  21051  reconnlem2  21831  lebnumlem3  21977  lebnumlem3OLD  21980  rrxmvallem  22344  itg1ge0a  22655  itg2seq  22686  m1lgs  24276  lmieu  24812  axlowdimlem14  24971  usgraidx2v  25106  cusgrafilem3  25194  cusgrafi  25195  usgrcyclnl1  25353  ex-natded5.13-2  25851  ordtconlem1  28725  eulerpartlemgh  29206  bnj23  29519  frind  30475  nn0prpw  30971  meran1  31063  poimirlem32  31885  heiborlem1  32056  riotaclbgBAD  32444  limclr  37555  eu2ndop1stv  38335  usgridx2v  38929  usgedgvadf1  38998  usgedgvadf1ALT  39001  mndpsuppss  39429
  Copyright terms: Public domain W3C validator