Theorem biancomi 467

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 465	. 2 ⊢ ((𝜓 ∧ 𝜒) ↔ (𝜒 ∧ 𝜓))
3	1, 2	bitr4i 281	1 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))

Syntax hints:   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  biantrur  539  rbaibr  546  pm4.71ri  569  anbi2ci  636  anbi1ci  637  anbi12ci  640  an12  657  an32  658  mpbiran2  722  3anan32  1111  eu6lem  2608  elon2  6375  fununi  6615  fnopabg  6676  eqfnfv3  7031  respreima  7065  fsn  7135  brtpos2  8231  tpostpos  8245  oeeu  8592  mapval2  8873  xrltlen  13174  ssfzoulel  13792  xpcogend  15014  dfgcd2  16607  isffth2  17978  resscntz  19406  fiidomfld  20861  1stcelcls  23601  txflf  24146  fclsrest  24164  tsmssubm  24283  blres  24571  xrtgioo  24947  isncvsngp  25291  itg1climres  25856  ellimc3  26021  lgsquadlem1  27524  lgsquadlem2  27525  wlkson  29974  0clwlk  30451  dmrab  32813  qusker  33639  bnj594  35270  kardexen  35534  satf0  35822  bj-elid6  37762  bj-imdirco  37782  wl-df4-3mintru2  38081  poimirlem4  38223  rabeqel  38856  iss2  38943  ifp1bi  44180  prprelprb  48215  prprspr2  48216  dfsclnbgr6  48572  dfidom2  49057  eliunxp2  49063