ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  bicom Structured version   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  601  con2bidc  762  con2biddc  767  pm5.17dc  803  bigolden  850  nbbndc  1268  bilukdc  1270  falbitru  1291  3impexpbicom  1306  exists1  1978  eqcom  2024  abeq1  2129  necon2abiddc  2249  necon2bbiddc  2250  necon4bbiddc  2257  ssequn1  3090  axpow3  3904  isocnv  5376
  Copyright terms: Public domain W3C validator