Theorem con4d 114

Description: Deduction associated with con4 112. (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

Step	Hyp	Ref	Expression
1		con4d.1	. 2 |- ( ph -> ( -. ps -> -. ch ) )
2		con4 112	. 2 |- ( ( -. ps -> -. ch ) -> ( ch -> ps ) )
3	1, 2	syl 17	1 |- ( ph -> ( ch -> ps ) )

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  118  pm2.18  122  con2d  129  con1d  139  mt4d  152  impcon4bid  217  con4bid  307  aleximi  1759  spc2gv  3296  spc3gv  3298  wfi  5713  soisoi  6578  isomin  6587  riotaclb  6649  extmptsuppeq  7319  mpt2xopynvov0g  7340  boxcutc  7951  sdomel  8107  onsdominel  8109  preleq  8514  cflim2  9085  cfslbn  9089  cofsmo  9091  fincssdom  9145  fin23lem25  9146  fin23lem26  9147  fin1a2s  9236  pwfseqlem4  9484  ltapr  9867  suplem2pr  9875  qsqueeze  12032  ssfzoulel  12562  ssnn0fi  12784  hashbnd  13123  hashclb  13149  hashgt0elex  13189  hashgt12el  13210  hashgt12el2  13211  pc2dvds  15583  infpnlem1  15614  odcl2  17982  ufilmax  21711  ufileu  21723  filufint  21724  hausflim  21785  flimfnfcls  21832  alexsubALTlem3  21853  alexsubALTlem4  21854  reconnlem2  22630  lebnumlem3  22762  rrxmvallem  23187  itg1ge0a  23478  itg2seq  23509  m1lgs  25113  lmieu  25676  axlowdimlem14  25835  usgredg2v  26119  cusgrfilem3  26353  cusgrfi  26354  vtxdgoddnumeven  26449  ex-natded5.13-2  27273  ordtconnlem1  29970  eulerpartlemgh  30440  bnj23  30784  frind  31740  nosepon  31818  nn0prpw  32318  meran1  32410  finxpreclem6  33233  wl-spae  33306  poimirlem32  33441  heiborlem1  33610  riotaclbgBAD  34240  reclt0  39614  limclr  39887  eu2ndop1stv  41202  mndpsuppss  42152