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

Theorem bicomi 130
Description: Inference from commutative law for logical equivalence. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 16-Sep-2013.)
Hypothesis
Ref Expression
bicomi.1  |-  ( ph  <->  ps )
Assertion
Ref Expression
bicomi  |-  ( ps  <->  ph )

Proof of Theorem bicomi
StepHypRef Expression
1 bicomi.1 . 2  |-  ( ph  <->  ps )
2 bicom1 129 . 2  |-  ( (
ph 
<->  ps )  ->  ( ps 
<-> 
ph ) )
31, 2ax-mp 7 1  |-  ( ps  <->  ph )
Colors of variables: wff set class
Syntax hints:    <-> 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
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  biimpri  131  bitr2i  183  bitr3i  184  bitr4i  185  syl5bbr  192  syl5rbbr  193  syl6bbr  196  syl6rbbr  197  pm5.41  249  anidm  388  pm4.87  524  anabs1  539  anabs7  541  pm4.76  571  mtbir  631  sylnibr  637  sylnbir  639  xchnxbir  641  xchbinxr  643  nbn  650  pm4.25  710  pm4.77  748  pm4.56  844  pm3.2an3  1122  syl3anbr  1218  3an6  1258  truan  1306  truimfal  1346  nottru  1349  sbid  1704  cleljust  1861  sb10f  1919  necon3bbii  2292  rspc2gv  2732  alexeq  2741  ceqsrexbv  2746  clel2  2748  clel4  2751  dfsbcq2  2841  cbvreucsf  2990  dfdif3  3108  raldifb  3138  difab  3266  un0  3314  in0  3315  ss0b  3319  iindif2m  3792  epse  4160  uniuni  4264  elco  4590  cotr  4800  issref  4801  mptpreima  4911  ralrnmpt  5425  rexrnmpt  5426  eroveu  6363  bdeq  11371  bd0r  11373  bdcriota  11431  bj-d0clsepcl  11477  bj-dfom  11485
  Copyright terms: Public domain W3C validator