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

Theorem bicomi 123
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
Assertion
Ref Expression
bicomi

Proof of Theorem bicomi
StepHypRef Expression
1 bicomi.1 . 2
2 bicom1 122 . 2
31, 2ax-mp 7 1
Colors of variables: wff set class
Syntax hints:   wb 98
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  biimpri  124  bitr2i  174  bitr3i  175  bitr4i  176  syl5bbr  183  syl5rbbr  184  syl6bbr  187  syl6rbbr  188  pm5.41  240  anidm  376  pm4.87  493  anabs1  506  anabs7  508  pm4.76  536  mtbir  595  sylnibr  601  sylnbir  603  xchnxbir  605  xchbinxr  607  nbn  614  pm4.25  674  pm4.77  711  pm4.56  805  pm3.2an3  1082  syl3anbr  1178  3an6  1216  truan  1259  truimfal  1298  nottru  1301  sbid  1654  cleljust  1810  sb10f  1868  necon3bbii  2236  alexeq  2664  ceqsrexbv  2669  clel2  2671  clel4  2674  dfsbcq2  2761  cbvreucsf  2904  raldifb  3077  difab  3200  un0  3245  in0  3246  ss0b  3250  iindif2m  3715  epse  4064  uniuni  4149  cotr  4649  issref  4650  mptpreima  4757  ralrnmpt  5252  rexrnmpt  5253  eroveu  6133  bdeq  9212  bd0r  9214  bdcriota  9272  bj-d0clsepcl  9314  bj-dfom  9321
  Copyright terms: Public domain W3C validator