Theorem con4d 109

Description: Deduction associated with con4 108. (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 108	. 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  110  pm2.18  114  con2d  120  con1d  129  mt4d  145  impcon4bid  210  con4bid  299  aleximi  1715  spc2gv  3149  spc3gv  3151  wfi  5432  soisoi  6244  isomin  6253  riotaclb  6314  extmptsuppeq  6966  mpt2xopynvov0g  6987  boxcutc  7591  sdomel  7745  onsdominel  7747  preleq  8148  cflim2  8719  cfslbn  8723  cofsmo  8725  fincssdom  8779  fin23lem25  8780  fin23lem26  8781  fin1a2s  8870  pwfseqlem4  9113  ltapr  9496  suplem2pr  9504  qsqueeze  11523  ssfzoulel  12036  ssnn0fi  12229  hashbnd  12553  hashclb  12572  hashgt0elex  12610  hashgt12el  12628  hashgt12el2  12629  pc2dvds  14877  infpnlem1  14903  odcl2  17265  ufilmax  20971  ufileu  20983  filufint  20984  hausflim  21045  flimfnfcls  21092  alexsubALTlem3  21113  alexsubALTlem4  21114  reconnlem2  21894  lebnumlem3  22040  lebnumlem3OLD  22043  rrxmvallem  22407  itg1ge0a  22718  itg2seq  22749  m1lgs  24339  lmieu  24875  axlowdimlem14  25034  usgraidx2v  25169  cusgrafilem3  25258  cusgrafi  25259  usgrcyclnl1  25417  ex-natded5.13-2  25915  ordtconlem1  28779  eulerpartlemgh  29260  bnj23  29573  frind  30530  nosepon  30605  nn0prpw  31028  meran1  31120  finxpreclem6  31833  poimirlem32  32017  heiborlem1  32188  riotaclbgBAD  32571  limclr  37774  eu2ndop1stv  38661  usgredg2v  39354  cusgrfilem3  39568  cusgrfi  39569  usgedgvadf1  40000  usgedgvadf1ALT  40003  mndpsuppss  40429