Theorem con4d 99

Description: Deduction derived from axiom ax-3 7. (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 7	. 2 |- ( ( -. ps -> -. ch ) -> ( ch -> ps ) )
3	1, 2	syl 16	1 |- ( ph -> ( ch -> ps ) )

Syntax hints:   -. wn 3   -> wi 4

This theorem is referenced by:  pm2.21d  100  pm2.18  104  con2d  109  con1d  118  mt4d  132  impcon4bid  197  con4bid  285  exim  1581  spOLD  1760  axi11e  2382  necon2ad  2615  spc2gv  2999  spc3gv  3001  soisoi  6007  isomin  6016  mpt2xopynvov0g  6424  riotaclbg  6548  boxcutc  7064  sdomel  7213  onsdominel  7215  preleq  7528  cantnfreslem  7587  cflim2  8099  cfslbn  8103  cofsmo  8105  fincssdom  8159  fin23lem25  8160  fin23lem26  8161  fin1a2s  8250  pwfseqlem4  8493  ltapr  8878  suplem2pr  8886  qsqueeze  10743  hashbnd  11579  hashclb  11596  hashgt0elex  11625  hashgt12el  11637  hashgt12el2  11638  pc2dvds  13207  infpnlem1  13233  odcl2  15156  ufilmax  17892  ufileu  17904  filufint  17905  hausflim  17966  flimfnfcls  18013  alexsubALTlem3  18033  alexsubALTlem4  18034  reconnlem2  18811  lebnumlem3  18941  itg1ge0a  19556  itg2seq  19587  m1lgs  21099  usgraidx2v  21365  cusgrafilem3  21443  cusgrafi  21444  usgrcyclnl1  21580  wfi  25421  frind  25457  axlowdimlem14  25798  meran1  26065  nn0prpw  26216  heiborlem1  26410  eu2ndop1stv  27847  bnj23  28789

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8