Theorem pm2.21d 624

Description: A contradiction implies anything. Deduction from pm2.21 622. (Contributed by NM, 10-Feb-1996.)

Hypothesis

Ref	Expression
pm2.21d.1	|- ( ph -> -. ps )

Assertion

Ref	Expression
pm2.21d	|- ( ph -> ( ps -> ch ) )

Proof of Theorem pm2.21d

Step	Hyp	Ref	Expression
1		pm2.21d.1	. 2 |- ( ph -> -. ps )
2		pm2.21 622	. 2 |- ( -. ps -> ( ps -> ch ) )
3	1, 2	syl 14	1 |- ( ph -> ( ps -> ch ) )

Syntax hints:   -. wn 3   -> wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-in2 620

This theorem is referenced by:  pm2.21dd  625  pm5.21  703  2falsed  710  mtord  791  prlem1  982  eq0rdv  3557  csbprc  3558  rzal  3611  ifeqeqxdc  3673  poirr2  5160  nnsucuniel  6741  nnawordex  6775  swoord2  6810  difinfsnlem  7403  exmidomni  7446  elni2  7645  cauappcvgprlemdisj  7982  caucvgprlemdisj  8005  caucvgprprlemdisj  8033  caucvgsr  8133  lelttr  8378  nnsub  9293  nn0ge2m1nn  9577  elnnz  9604  elnn0z  9607  indstr  9943  indstr2  9959  xrltnsym  10145  xrlttr  10147  xrltso  10148  xrlelttr  10158  xltnegi  10187  xsubge0  10233  ixxdisj  10255  icodisj  10344  fzm1  10456  qbtwnxr  10641  frec2uzlt2d  10790  nn0ltexp2  11096  facdiv  11125  resqrexlemgt0  11730  climuni  12003  fsumcl2lem  12109  dvdsle  12555  prmdvdsexpr  12872  prmfac1  12874  sqrt2irr  12884  phibndlem  12938  dvdsprmpweqle  13060  isxmet2d  15339  lgsdir2lem2  16028  lgseisenlem2  16070  wlkv0  16490  trilpolemres  16952