Theorem pm2.21d 615

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

This theorem is referenced by:  pm2.21dd  616  pm5.21  691  2falsed  698  mtord  779  prlem1  969  eq0rdv  3460  csbprc  3461  rzal  3513  poirr2  5005  nnsucuniel  6478  nnawordex  6512  swoord2  6547  difinfsnlem  7080  exmidomni  7122  elni2  7280  cauappcvgprlemdisj  7617  caucvgprlemdisj  7640  caucvgprprlemdisj  7668  caucvgsr  7768  lelttr  8012  nnsub  8921  nn0ge2m1nn  9199  elnnz  9226  elnn0z  9229  indstr  9556  indstr2  9572  xrltnsym  9754  xrlttr  9756  xrltso  9757  xrlelttr  9767  xltnegi  9796  xsubge0  9842  ixxdisj  9864  icodisj  9953  fzm1  10060  qbtwnxr  10218  frec2uzlt2d  10364  nn0ltexp2  10648  facdiv  10676  resqrexlemgt0  10988  climuni  11260  fsumcl2lem  11365  dvdsle  11808  prmdvdsexpr  12108  prmfac1  12110  sqrt2irr  12120  phibndlem  12174  dvdsprmpweqle  12294  isxmet2d  13227  lgsdir2lem2  13809  trilpolemres  14159