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

Theorem imnan 634
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 576 . . . 4  |-  ( ph  ->  ( ps  ->  -.  ( ph  ->  -.  ps )
) )
21imp 119 . . 3  |-  ( (
ph  /\  ps )  ->  -.  ( ph  ->  -. 
ps ) )
32con2i 567 . 2  |-  ( (
ph  ->  -.  ps )  ->  -.  ( ph  /\  ps ) )
4 pm3.2 130 . . 3  |-  ( ph  ->  ( ps  ->  ( ph  /\  ps ) ) )
54con3rr3 573 . 2  |-  ( -.  ( ph  /\  ps )  ->  ( ph  ->  -. 
ps ) )
63, 5impbii 121 1  |-  ( (
ph  ->  -.  ps )  <->  -.  ( ph  /\  ps ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 101    <-> wb 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-in1 554  ax-in2 555
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  imnani  635  nan  636  pm3.24  637  imandc  797  ianordc  810  pm5.17dc  821  dn1dc  878  xorbin  1291  xordc1  1300  alinexa  1510  ralinexa  2368  pssn2lp  3073  rabeq0  3275  disj  3296  minel  3311  disjsn  3460  sotricim  4088  poirr2  4745  funun  4972  imadiflem  5006  imadif  5007  brprcneu  5199  prltlu  6643  caucvgprlemnbj  6823  caucvgprprlemnbj  6849  xrltnsym2  8816  fzp1nel  9068
  Copyright terms: Public domain W3C validator