Theorem intnanrd 927

Description: Introduction of conjunct inside of a contradiction. (Contributed by NM, 10-Jul-2005.)

Hypothesis

Ref	Expression
intnand.1	|- ( ph -> -. ps )

Assertion

Ref	Expression
intnanrd	|- ( ph -> -. ( ps /\ ch ) )

Proof of Theorem intnanrd

Step	Hyp	Ref	Expression
1		intnand.1	. 2 |- ( ph -> -. ps )
2		simpl 108	. 2 |- ( ( ps /\ ch ) -> ps )
3	1, 2	nsyl 623	1 |- ( ph -> -. ( ps /\ ch ) )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-in1 609  ax-in2 610

This theorem is referenced by:  dcan  928  bianfd  943  frecabcl  6378  frecsuclem  6385  xrrebnd  9776  fzpreddisj  10027  iseqf1olemqk  10450  gcdsupex  11912  gcdsupcl  11913  nndvdslegcd  11920  divgcdnn  11930  sqgcd  11984  coprm  12098  pclemdc  12242  1arith  12319  ctiunctlemudc  12392  lgsval2lem  13705  lgsval4a  13717  lgsdilem  13722