Theorem pm2.21d 622

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

This theorem is referenced by:  pm2.21dd  623  pm5.21  700  2falsed  707  mtord  788  prlem1  979  eq0rdv  3537  csbprc  3538  rzal  3590  poirr2  5127  nnsucuniel  6658  nnawordex  6692  swoord2  6727  difinfsnlem  7289  exmidomni  7332  elni2  7524  cauappcvgprlemdisj  7861  caucvgprlemdisj  7884  caucvgprprlemdisj  7912  caucvgsr  8012  lelttr  8258  nnsub  9172  nn0ge2m1nn  9452  elnnz  9479  elnn0z  9482  indstr  9817  indstr2  9833  xrltnsym  10018  xrlttr  10020  xrltso  10021  xrlelttr  10031  xltnegi  10060  xsubge0  10106  ixxdisj  10128  icodisj  10217  fzm1  10325  qbtwnxr  10507  frec2uzlt2d  10656  nn0ltexp2  10961  facdiv  10990  resqrexlemgt0  11571  climuni  11844  fsumcl2lem  11949  dvdsle  12395  prmdvdsexpr  12712  prmfac1  12714  sqrt2irr  12724  phibndlem  12778  dvdsprmpweqle  12900  isxmet2d  15062  lgsdir2lem2  15748  lgseisenlem2  15790  wlkv0  16166  trilpolemres  16582