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

Theorem bicomi 131
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 130 . 2  |-  ( (
ph 
<->  ps )  ->  ( ps 
<-> 
ph ) )
31, 2ax-mp 5 1  |-  ( ps  <->  ph )
Colors of variables: wff set class
Syntax hints:    <-> 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
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  biimpri  132  bitr2i  184  bitr3i  185  bitr4i  186  bitr3id  193  bitr3di  194  bitr4di  197  bitr4id  198  pm5.41  250  anidm  394  pm4.87  547  anabs1  562  anabs7  564  pm4.76  594  mtbir  661  sylnibr  667  sylnbir  669  xchnxbir  671  xchbinxr  673  nbn  689  pm4.25  748  pm4.56  770  pm4.77  789  pm3.2an3  1161  syl3anbr  1264  3an6  1304  truan  1352  truimfal  1392  nottru  1395  sbid  1754  sb10f  1975  cleljust  2134  nfabdw  2318  necon3bbii  2364  rspc2gv  2828  alexeq  2838  ceqsrexbv  2843  clel2  2845  clel4  2848  dfsbcq2  2940  cbvreucsf  3095  dfdif3  3217  raldifb  3247  difab  3376  un0  3427  in0  3428  ss0b  3433  rexdifpr  3588  iindif2m  3916  epse  4302  abnex  4407  uniuni  4411  elco  4752  cotr  4967  issref  4968  mptpreima  5079  ralrnmpt  5609  rexrnmpt  5610  eroveu  6571  fprodseq  11480  toptopon  12427  xmeterval  12846  txmetcnp  12929  dedekindicclemicc  13021  eldvap  13062  if0ab  13391  bdeq  13409  bd0r  13411  bdcriota  13469  bj-d0clsepcl  13511  bj-dfom  13519
  Copyright terms: Public domain W3C validator