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

Theorem imnan 659
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 601 . . . 4  |-  ( ph  ->  ( ps  ->  -.  ( ph  ->  -.  ps )
) )
21imp 122 . . 3  |-  ( (
ph  /\  ps )  ->  -.  ( ph  ->  -. 
ps ) )
32con2i 592 . 2  |-  ( (
ph  ->  -.  ps )  ->  -.  ( ph  /\  ps ) )
4 pm3.2 137 . . 3  |-  ( ph  ->  ( ps  ->  ( ph  /\  ps ) ) )
54con3rr3 598 . 2  |-  ( -.  ( ph  /\  ps )  ->  ( ph  ->  -. 
ps ) )
63, 5impbii 124 1  |-  ( (
ph  ->  -.  ps )  <->  -.  ( ph  /\  ps ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 102    <-> wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 579  ax-in2 580
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  imnani  660  nan  661  pm3.24  662  imanst  779  imandc  824  ianordc  837  pm5.17dc  848  dn1dc  906  xorbin  1320  xordc1  1329  alinexa  1539  dfrex2dc  2371  ralinexa  2405  rabeq0  3310  disj  3328  minel  3341  disjsn  3499  sotricim  4141  poirr2  4811  funun  5044  imadiflem  5079  imadif  5080  brprcneu  5282  prltlu  7025  caucvgprlemnbj  7205  caucvgprprlemnbj  7231  xrltnsym2  9233  fzp1nel  9485  fsumsplit  10764  sumsplitdc  10789  phiprmpw  11291
  Copyright terms: Public domain W3C validator