Theorem bicom 222

Description: Commutative law for the biconditional. Theorem *4.21 of [WhiteheadRussell] p. 117. (Contributed by NM, 11-May-1993.)

Assertion

Ref	Expression
bicom	⊢ ((𝜑 ↔ 𝜓) ↔ (𝜓 ↔ 𝜑))

Proof of Theorem bicom

Step	Hyp	Ref	Expression
1		bicom1 221	. 2 ⊢ ((𝜑 ↔ 𝜓) → (𝜓 ↔ 𝜑))
2		bicom1 221	. 2 ⊢ ((𝜓 ↔ 𝜑) → (𝜑 ↔ 𝜓))
3	1, 2	impbii 209	1 ⊢ ((𝜑 ↔ 𝜓) ↔ (𝜓 ↔ 𝜑))

Syntax hints:   ↔ wb 206

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207

This theorem is referenced by:  bicomd  223  bibi1i  338  bibi1d  343  con2bi  353  ibibr  368  bibif  371  nbbn  383  biluk  385  biadan  819  pm5.17  1014  bigolden  1029  xorcom  1514  norass  1537  trubifal  1571  hadcoma  1599  eqabcb  2883  pm13.183  3666  ssequn1  4186  ab0w  4379  disj  4450  isocnv  7350  qextlt  13245  qextle  13246  rpnnen2lem12  16261  odd2np1  16378  sumodd  16425  nrmmetd  24587  lgsqrmodndvds  27397  eqelbid  32494  mgccnv  32989  cvmlift2lem12  35319  nn0prpw  36324  wl-3xorrot  37478  wl-3xorcoma  37479  tsbi4  38143  bicomdd  38855  onsupmaxb  43251  ifpbicor  43488  rp-fakeoranass  43527  or3or  44036  3impexpbicom  44500  3impexpbicomVD  44877  notbicom  45170  limsupreuz  45752  nabctnabc  46943