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  1622  eximOLD  1624  necon2ad  2664  spc2gv  3065  spc3gv  3067  soisoi  6024  isomin  6033  riotaclb  6095  extmptsuppeq  6718  mpt2xopynvov0g  6736  boxcutc  7311  sdomel  7463  onsdominel  7465  preleq  7828  cflim2  8437  cfslbn  8441  cofsmo  8443  fincssdom  8497  fin23lem25  8498  fin23lem26  8499  fin1a2s  8588  pwfseqlem4  8834  ltapr  9219  suplem2pr  9227  qsqueeze  11176  ssfzoulel  11626  hashbnd  12114  hashclb  12133  hashgt0elex  12164  hashgt12el  12178  hashgt12el2  12179  pc2dvds  13950  infpnlem1  13976  odcl2  16071  ufilmax  19485  ufileu  19497  filufint  19498  hausflim  19559  flimfnfcls  19606  alexsubALTlem3  19626  alexsubALTlem4  19627  reconnlem2  20409  lebnumlem3  20540  rrxmvallem  20908  itg1ge0a  21194  itg2seq  21225  m1lgs  22706  axlowdimlem14  23206  usgraidx2v  23316  cusgrafilem3  23394  cusgrafi  23395  usgrcyclnl1  23531  ex-natded5.13-2  23628  ordtconlem1  26359  eulerpartlemgh  26766  wfi  27673  frind  27709  meran1  28262  nn0prpw  28523  heiborlem1  28715  eu2ndop1stv  30031  ssnn0fi  30751  mndpsuppss  30789  bnj23  31712  riotaclbgBAD  32610  riotaclbBAD  32611