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

Theorem bicom 138
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 129 . 2 ((𝜑𝜓) → (𝜓𝜑))
2 bicom1 129 . 2 ((𝜓𝜑) → (𝜑𝜓))
31, 2impbii 124 1 ((𝜑𝜓) ↔ (𝜓𝜑))
Colors of variables: wff set class
Syntax hints:  wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  bicomd  139  bibi1i  226  bibi1d  231  ibibr  244  bibif  647  con2bidc  805  con2biddc  810  pm5.17dc  846  bigolden  899  nbbndc  1328  bilukdc  1330  falbitru  1351  3impexpbicom  1370  exists1  2041  eqcom  2087  abeq1  2194  necon2abiddc  2317  necon2bbiddc  2318  necon4bbiddc  2325  ssequn1  3159  axpow3  3987  isocnv  5551  bezoutlemle  10879
  Copyright terms: Public domain W3C validator