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

Theorem con4d 105
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 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  106  pm2.18  110  con2d  115  con1d  124  mt4d  138  impcon4bid  205  con4bid  293  aleximi  1654  eximOLD  1656  necon2adOLD  2671  spc2gv  3197  spc3gv  3199  soisoi  6225  isomin  6234  riotaclb  6295  extmptsuppeq  6942  mpt2xopynvov0g  6960  boxcutc  7531  sdomel  7683  onsdominel  7685  preleq  8051  cflim2  8660  cfslbn  8664  cofsmo  8666  fincssdom  8720  fin23lem25  8721  fin23lem26  8722  fin1a2s  8811  pwfseqlem4  9057  ltapr  9440  suplem2pr  9448  qsqueeze  11425  ssfzoulel  11908  ssnn0fi  12096  hashbnd  12413  hashclb  12432  hashgt0elex  12469  hashgt12el  12484  hashgt12el2  12485  pc2dvds  14413  infpnlem1  14439  odcl2  16713  ufilmax  20533  ufileu  20545  filufint  20546  hausflim  20607  flimfnfcls  20654  alexsubALTlem3  20674  alexsubALTlem4  20675  reconnlem2  21457  lebnumlem3  21588  rrxmvallem  21956  itg1ge0a  22243  itg2seq  22274  m1lgs  23762  lmieu  24275  axlowdimlem14  24384  usgraidx2v  24519  cusgrafilem3  24607  cusgrafi  24608  usgrcyclnl1  24766  ex-natded5.13-2  25263  ordtconlem1  28059  eulerpartlemgh  28492  wfi  29461  frind  29497  meran1  30038  nn0prpw  30303  heiborlem1  30469  limclr  31822  eu2ndop1stv  32368  usgedgvadf1  32635  usgedgvadf1ALT  32638  mndpsuppss  33066  bnj23  33872  riotaclbgBAD  34786
  Copyright terms: Public domain W3C validator