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

Theorem con4d 97
Description: Deduction derived from axiom ax-3 7. (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 7 . 2  |-  ( ( -.  ps  ->  -.  ch )  ->  ( ch 
->  ps ) )
31, 2syl 15 1  |-  ( ph  ->  ( ch  ->  ps ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  pm2.21d  98  pm2.18  102  con2d  107  con1d  116  mt4d  130  impcon4bid  196  con4bid  284  exim  1564  sp  1718  necon2ad  2496  spc2gv  2873  spc3gv  2875  soisoi  5827  isomin  5836  riotaclbg  6346  boxcutc  6861  sdomel  7010  onsdominel  7012  preleq  7320  cantnfreslem  7379  cflim2  7891  cfslbn  7895  cofsmo  7897  fincssdom  7951  fin23lem25  7952  fin23lem26  7953  fin1a2s  8042  pwfseqlem4  8286  ltapr  8671  suplem2pr  8679  qsqueeze  10530  hashbnd  11345  hashclb  11354  sadcaddlem  12650  pc2dvds  12933  infpnlem1  12959  odcl2  14880  ufilmax  17604  ufileu  17616  filufint  17617  hausflim  17678  flimfnfcls  17725  alexsubALTlem3  17745  alexsubALTlem4  17746  reconnlem2  18334  lebnumlem3  18463  itg1ge0a  19068  itg2seq  19099  m1lgs  20603  ex-natded5.13-2  20805  wfi  24209  frind  24245  axlowdimlem14  24585  meran1  24852  iintlem1  25621  lvsovso2  25638  nn0prpw  26250  heiborlem1  26546  mpt2xopynvov0g  28091  bnj23  28817  a12study10  29209  a12study10n  29210  ax9lem3  29215
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator