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

Theorem bicom 140
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 131 . 2 ((𝜑𝜓) → (𝜓𝜑))
2 bicom1 131 . 2 ((𝜓𝜑) → (𝜑𝜓))
31, 2impbii 126 1 ((𝜑𝜓) ↔ (𝜓𝜑))
Colors of variables: wff set class
Syntax hints:  wb 105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  bicomd  141  bibi1i  228  bibi1d  233  ibibr  246  bibif  699  con2bidc  876  con2biddc  881  pm5.17dc  905  bigolden  956  nbbndc  1404  bilukdc  1406  falbitru  1427  3impexpbicom  1448  exists1  2133  eqcom  2190  abeq1  2298  necon2abiddc  2425  necon2bbiddc  2426  necon4bbiddc  2433  ssequn1  3319  axpow3  4191  isocnv  5827  suplocsrlem  7824  uzennn  10453  bezoutlemle  12026
  Copyright terms: Public domain W3C validator