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  1632  eximOLD  1634  necon2adOLD  2681  spc2gv  3201  spc3gv  3203  soisoi  6210  isomin  6219  riotaclb  6281  extmptsuppeq  6921  mpt2xopynvov0g  6939  boxcutc  7509  sdomel  7661  onsdominel  7663  preleq  8030  cflim2  8639  cfslbn  8643  cofsmo  8645  fincssdom  8699  fin23lem25  8700  fin23lem26  8701  fin1a2s  8790  pwfseqlem4  9036  ltapr  9419  suplem2pr  9427  qsqueeze  11396  ssfzoulel  11870  ssnn0fi  12058  hashbnd  12375  hashclb  12394  hashgt0elex  12428  hashgt12el  12442  hashgt12el2  12443  pc2dvds  14257  infpnlem1  14283  odcl2  16383  ufilmax  20143  ufileu  20155  filufint  20156  hausflim  20217  flimfnfcls  20264  alexsubALTlem3  20284  alexsubALTlem4  20285  reconnlem2  21067  lebnumlem3  21198  rrxmvallem  21566  itg1ge0a  21853  itg2seq  21884  m1lgs  23365  lmieu  23827  axlowdimlem14  23934  usgraidx2v  24069  cusgrafilem3  24157  cusgrafi  24158  usgrcyclnl1  24316  ex-natded5.13-2  24814  ordtconlem1  27542  eulerpartlemgh  27957  wfi  28864  frind  28900  meran1  29453  nn0prpw  29718  heiborlem1  29910  limclr  31197  fourierdlem79  31486  eu2ndop1stv  31674  usgedgvadf1  31884  usgedgvadf1ALT  31887  mndpsuppss  32037  bnj23  32851  riotaclbgBAD  33757  riotaclbBAD  33758