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  1562  sp  1717  necon2ad  2495  spc2gv  2872  spc3gv  2874  soisoi  5787  isomin  5796  riotaclbg  6340  boxcutc  6855  sdomel  7004  onsdominel  7006  preleq  7314  cantnfreslem  7373  cflim2  7885  cfslbn  7889  cofsmo  7891  fincssdom  7945  fin23lem25  7946  fin23lem26  7947  fin1a2s  8036  pwfseqlem4  8280  ltapr  8665  suplem2pr  8673  qsqueeze  10524  hashbnd  11339  hashclb  11348  sadcaddlem  12644  pc2dvds  12927  infpnlem1  12953  odcl2  14874  ufilmax  17598  ufileu  17610  filufint  17611  hausflim  17672  flimfnfcls  17719  alexsubALTlem3  17739  alexsubALTlem4  17740  reconnlem2  18328  lebnumlem3  18457  itg1ge0a  19062  itg2seq  19093  m1lgs  20597  ex-natded5.13-2  20825  wfi  23611  frind  23647  axlowdimlem14  23993  meran1  24260  iintlem1  25021  lvsovso2  25038  nn0prpw  25650  heiborlem1  25946  bnj23  28023  a12study10  28415  a12study10n  28416  ax9lem3  28421
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator