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

Theorem imnan 660
Description: Express implication in terms of conjunction. (Contributed by NM, 9-Apr-1994.) (Revised by Mario Carneiro, 1-Feb-2015.)
Assertion
Ref Expression
imnan  |-  ( (
ph  ->  -.  ps )  <->  -.  ( ph  /\  ps ) )

Proof of Theorem imnan
StepHypRef Expression
1 pm3.2im 602 . . . 4  |-  ( ph  ->  ( ps  ->  -.  ( ph  ->  -.  ps )
) )
21imp 123 . . 3  |-  ( (
ph  /\  ps )  ->  -.  ( ph  ->  -. 
ps ) )
32con2i 593 . 2  |-  ( (
ph  ->  -.  ps )  ->  -.  ( ph  /\  ps ) )
4 pm3.2 138 . . 3  |-  ( ph  ->  ( ps  ->  ( ph  /\  ps ) ) )
54con3rr3 599 . 2  |-  ( -.  ( ph  /\  ps )  ->  ( ph  ->  -. 
ps ) )
63, 5impbii 125 1  |-  ( (
ph  ->  -.  ps )  <->  -.  ( ph  /\  ps ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 103    <-> wb 104
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 580  ax-in2 581
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  imnani  661  nan  662  pm3.24  663  imanst  780  imandc  825  ianordc  838  pm5.17dc  849  dn1dc  907  xorbin  1321  xordc1  1330  alinexa  1540  dfrex2dc  2372  ralinexa  2406  rabeq0  3318  disj  3337  minel  3350  disjsn  3510  sotricim  4161  poirr2  4839  funun  5073  imadiflem  5108  imadif  5109  brprcneu  5313  prltlu  7109  caucvgprlemnbj  7289  caucvgprprlemnbj  7315  xrltnsym2  9327  fzp1nel  9581  fsumsplit  10864  sumsplitdc  10889  phiprmpw  11539
  Copyright terms: Public domain W3C validator