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

Theorem bicom 132
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 126 . 2 ((𝜑𝜓) → (𝜓𝜑))
2 bicom1 126 . 2 ((𝜓𝜑) → (𝜑𝜓))
31, 2impbii 121 1 ((𝜑𝜓) ↔ (𝜓𝜑))
Colors of variables: wff set class
Syntax hints:  wb 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  bicomd  133  bibi1i  221  bibi1d  226  ibibr  239  bibif  624  con2bidc  780  con2biddc  785  pm5.17dc  821  bigolden  873  nbbndc  1301  bilukdc  1303  falbitru  1324  3impexpbicom  1343  exists1  2012  eqcom  2058  abeq1  2163  necon2abiddc  2286  necon2bbiddc  2287  necon4bbiddc  2294  ssequn1  3141  axpow3  3958  isocnv  5479
  Copyright terms: Public domain W3C validator