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  818  pm5.17  1013  bigolden  1028  xorcom  1514  norass  1537  trubifal  1571  hadcoma  1599  eqabcb  2869  pm13.183  3629  ssequn1  4145  ab0w  4338  disj  4409  isocnv  7287  qextlt  13139  qextle  13140  rpnnen2lem12  16169  odd2np1  16287  sumodd  16334  nrmmetd  24495  lgsqrmodndvds  27297  eqelbid  32454  mgccnv  32971  cvmlift2lem12  35294  nn0prpw  36304  wl-3xorrot  37458  wl-3xorcoma  37459  tsbi4  38123  bicomdd  38840  onsupmaxb  43221  ifpbicor  43457  rp-fakeoranass  43496  or3or  44005  3impexpbicom  44463  3impexpbicomVD  44839  notbicom  45152  limsupreuz  45728  nabctnabc  46925