Theorem biancomi 461

Description: Commuting conjunction in a biconditional. (Contributed by Peter Mazsa, 17-Jun-2018.)

Hypothesis

Ref	Expression
biancomi.1	⊢ (𝜑 ↔ (𝜒 ∧ 𝜓))

Assertion

Ref	Expression
biancomi	⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))

Proof of Theorem biancomi

Step	Hyp	Ref	Expression
1		biancomi.1	. 2 ⊢ (𝜑 ↔ (𝜒 ∧ 𝜓))
2		ancom 459	. 2 ⊢ ((𝜓 ∧ 𝜒) ↔ (𝜒 ∧ 𝜓))
3	1, 2	bitr4i 277	1 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))

Syntax hints:   ↔ wb 205   ∧ wa 394

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 206  df-an 395

This theorem is referenced by:  biantrur  529  rbaibr  536  pm4.71ri  559  anbi2ci  623  anbi1ci  624  anbi12ci  627  an12  643  an32  644  mpbiran2  708  eu6lem  2561  elon2  6380  fununi  6627  fnopabg  6691  eqfnfv3  7039  respreima  7072  fsn  7142  brtpos2  8236  tpostpos  8250  oeeu  8622  mapval2  8889  xrltlen  13157  ssfzoulel  13758  xpcogend  14953  dfgcd2  16521  isffth2  17904  resscntz  19288  fiidomfld  21266  1stcelcls  23395  txflf  23940  fclsrest  23958  tsmssubm  24077  blres  24367  xrtgioo  24752  isncvsngp  25107  itg1climres  25674  ellimc3  25838  lgsquadlem1  27343  lgsquadlem2  27344  wlkson  29526  0clwlk  29996  dmrab  32352  qusker  33121  bnj594  34613  satf0  35052  bj-elid6  36719  bj-imdirco  36739  wl-df4-3mintru2  37036  poimirlem4  37167  rabeqel  37795  iss2  37885  ifp1bi  42997  prprelprb  46920  prprspr2  46921  dfsclnbgr6  47256  eliunxp2  47509