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

Step	Hyp	Ref	Expression
1		con4d.1	. 2 |- ( ph -> ( -. ps -> -. ch ) )
2		ax-3 8	. 2 |- ( ( -. ps -> -. ch ) -> ( ch -> ps ) )
3	1, 2	syl 16	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  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