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

Theorem bicom 128
Description: Commutative law for equivalence. Theorem *4.21 of [WhiteheadRussell] p. 117. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 11-Nov-2012.)
Assertion
Ref Expression
bicom

Proof of Theorem bicom
StepHypRef Expression
1 bicom1 122 . 2
2 bicom1 122 . 2
31, 2impbii 117 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:  bicomd  129  bibi1i  217  bibi1d  222  ibibr  235  bibif  613  con2bidc  768  con2biddc  773  pm5.17dc  809  bigolden  861  nbbndc  1282  bilukdc  1284  falbitru  1305  3impexpbicom  1324  exists1  1993  eqcom  2039  abeq1  2144  necon2abiddc  2265  necon2bbiddc  2266  necon4bbiddc  2273  ssequn1  3107  axpow3  3921  isocnv  5394
  Copyright terms: Public domain W3C validator