Theorem pm2.21d 609

Description: A contradiction implies anything. Deduction from pm2.21 607. (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 607	. 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 605

This theorem is referenced by:  pm2.21dd  610  pm5.21  685  2falsed  692  mtord  773  prlem1  958  eq0rdv  3412  csbprc  3413  rzal  3465  poirr2  4939  nnsucuniel  6399  nnawordex  6432  swoord2  6467  difinfsnlem  6992  exmidomni  7022  elni2  7146  cauappcvgprlemdisj  7483  caucvgprlemdisj  7506  caucvgprprlemdisj  7534  caucvgsr  7634  lelttr  7876  nnsub  8783  nn0ge2m1nn  9061  elnnz  9088  elnn0z  9091  indstr  9415  indstr2  9430  xrltnsym  9609  xrlttr  9611  xrltso  9612  xrlelttr  9619  xltnegi  9648  xsubge0  9694  ixxdisj  9716  icodisj  9805  fzm1  9911  qbtwnxr  10066  frec2uzlt2d  10208  facdiv  10516  resqrexlemgt0  10824  climuni  11094  fsumcl2lem  11199  dvdsle  11578  prmdvdsexpr  11864  prmfac1  11866  sqrt2irr  11876  phibndlem  11928  isxmet2d  12556  trilpolemres  13410