ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  intnanrd GIF version

Theorem intnanrd 927
Description: Introduction of conjunct inside of a contradiction. (Contributed by NM, 10-Jul-2005.)
Hypothesis
Ref Expression
intnand.1 (𝜑 → ¬ 𝜓)
Assertion
Ref Expression
intnanrd (𝜑 → ¬ (𝜓𝜒))

Proof of Theorem intnanrd
StepHypRef Expression
1 intnand.1 . 2 (𝜑 → ¬ 𝜓)
2 simpl 108 . 2 ((𝜓𝜒) → 𝜓)
31, 2nsyl 623 1 (𝜑 → ¬ (𝜓𝜒))
Colors of variables: wff set class
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
  Copyright terms: Public domain W3C validator