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

Theorem imnan 679
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 626 . . . 4  |-  ( ph  ->  ( ps  ->  -.  ( ph  ->  -.  ps )
) )
21imp 123 . . 3  |-  ( (
ph  /\  ps )  ->  -.  ( ph  ->  -. 
ps ) )
32con2i 616 . 2  |-  ( (
ph  ->  -.  ps )  ->  -.  ( ph  /\  ps ) )
4 pm3.2 138 . . 3  |-  ( ph  ->  ( ps  ->  ( ph  /\  ps ) ) )
54con3rr3 622 . 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-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 603  ax-in2 604
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  imnani  680  nan  681  pm3.24  682  imanst  873  ianordc  884  pm5.17dc  889  dn1dc  944  xorbin  1362  xordc1  1371  alinexa  1582  dfrex2dc  2428  ralinexa  2462  rabeq0  3392  disj  3411  minel  3424  disjsn  3585  sotricim  4245  poirr2  4931  funun  5167  imadiflem  5202  imadif  5203  brprcneu  5414  prltlu  7302  caucvgprlemnbj  7482  caucvgprprlemnbj  7508  suplocexprlemmu  7533  xrltnsym2  9587  fzp1nel  9891  fsumsplit  11183  sumsplitdc  11208  phiprmpw  11905  bj-nnor  12976
  Copyright terms: Public domain W3C validator