Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  bicom GIF 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  614  con2bidc  769  con2biddc  774  pm5.17dc  810  bigolden  862  nbbndc  1285  bilukdc  1287  falbitru  1308  3impexpbicom  1327  exists1  1996  eqcom  2042  abeq1  2147  necon2abiddc  2271  necon2bbiddc  2272  necon4bbiddc  2279  ssequn1  3113  axpow3  3930  isocnv  5451
 Copyright terms: Public domain W3C validator