Theorem pm2.21d 620

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

This theorem is referenced by:  pm2.21dd  621  pm5.21  697  2falsed  704  mtord  785  prlem1  976  eq0rdv  3509  csbprc  3510  rzal  3562  poirr2  5089  nnsucuniel  6599  nnawordex  6633  swoord2  6668  difinfsnlem  7222  exmidomni  7265  elni2  7457  cauappcvgprlemdisj  7794  caucvgprlemdisj  7817  caucvgprprlemdisj  7845  caucvgsr  7945  lelttr  8191  nnsub  9105  nn0ge2m1nn  9385  elnnz  9412  elnn0z  9415  indstr  9744  indstr2  9760  xrltnsym  9945  xrlttr  9947  xrltso  9948  xrlelttr  9958  xltnegi  9987  xsubge0  10033  ixxdisj  10055  icodisj  10144  fzm1  10252  qbtwnxr  10432  frec2uzlt2d  10581  nn0ltexp2  10886  facdiv  10915  resqrexlemgt0  11416  climuni  11689  fsumcl2lem  11794  dvdsle  12240  prmdvdsexpr  12557  prmfac1  12559  sqrt2irr  12569  phibndlem  12623  dvdsprmpweqle  12745  isxmet2d  14905  lgsdir2lem2  15591  lgseisenlem2  15633  trilpolemres  16153