ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  bicomi GIF 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 (𝜑𝜓)
Assertion
Ref Expression
bicomi (𝜓𝜑)

Proof of Theorem bicomi
StepHypRef Expression
1 bicomi.1 . 2 (𝜑𝜓)
2 bicom1 130 . 2 ((𝜑𝜓) → (𝜓𝜑))
31, 2ax-mp 5 1 (𝜓𝜑)
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  syl5bbr  193  syl5rbbr  194  syl6bbr  197  syl6rbbr  198  pm5.41  250  anidm  391  pm4.87  529  anabs1  544  anabs7  546  pm4.76  576  mtbir  643  sylnibr  649  sylnbir  651  xchnxbir  653  xchbinxr  655  nbn  671  pm4.25  730  pm4.56  752  pm4.77  771  pm3.2an3  1143  syl3anbr  1243  3an6  1283  truan  1331  truimfal  1371  nottru  1374  sbid  1730  cleljust  1888  sb10f  1946  necon3bbii  2320  rspc2gv  2773  alexeq  2783  ceqsrexbv  2788  clel2  2790  clel4  2793  dfsbcq2  2883  cbvreucsf  3032  dfdif3  3154  raldifb  3184  difab  3313  un0  3364  in0  3365  ss0b  3370  iindif2m  3848  epse  4232  abnex  4336  uniuni  4340  elco  4673  cotr  4888  issref  4889  mptpreima  5000  ralrnmpt  5528  rexrnmpt  5529  eroveu  6486  toptopon  12091  xmeterval  12510  txmetcnp  12593  dedekindicclemicc  12685  eldvap  12726  bdeq  12855  bd0r  12857  bdcriota  12915  bj-d0clsepcl  12957  bj-dfom  12965
  Copyright terms: Public domain W3C validator