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

Theorem bicom 139
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 130 . 2 ((𝜑𝜓) → (𝜓𝜑))
2 bicom1 130 . 2 ((𝜓𝜑) → (𝜑𝜓))
31, 2impbii 125 1 ((𝜑𝜓) ↔ (𝜓𝜑))
Colors of variables: wff set class
Syntax hints:  wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  bicomd  140  bibi1i  227  bibi1d  232  ibibr  245  bibif  687  con2bidc  860  con2biddc  865  pm5.17dc  889  bigolden  939  nbbndc  1372  bilukdc  1374  falbitru  1395  3impexpbicom  1414  exists1  2095  eqcom  2141  abeq1  2249  necon2abiddc  2374  necon2bbiddc  2375  necon4bbiddc  2382  ssequn1  3246  axpow3  4101  isocnv  5712  suplocsrlem  7628  uzennn  10221  bezoutlemle  11707
  Copyright terms: Public domain W3C validator