Theorem biancomi 463

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

Syntax hints:   ↔ wb 205   ∧ wa 396

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 397

This theorem is referenced by:  biantrur  531  rbaibr  538  pm4.71ri  561  anbi2ci  625  anbi1ci  626  anbi12ci  628  an12  643  an32  644  mpbiran2  708  eu6lem  2566  elon2  6333  fununi  6581  fnopabg  6643  eqfnfv3  6989  respreima  7021  fsn  7086  brtpos2  8168  tpostpos  8182  oeeu  8555  mapval2  8817  xrltlen  13075  ssfzoulel  13676  xpcogend  14871  dfgcd2  16438  isffth2  17817  resscntz  19126  fiidomfld  20816  1stcelcls  22849  txflf  23394  fclsrest  23412  tsmssubm  23531  blres  23821  xrtgioo  24206  isncvsngp  24550  itg1climres  25116  ellimc3  25280  lgsquadlem1  26765  lgsquadlem2  26766  wlkson  28667  0clwlk  29137  dmrab  31489  qusker  32212  bnj594  33613  satf0  34053  bj-elid6  35714  bj-imdirco  35734  wl-df4-3mintru2  36031  poimirlem4  36155  rabeqel  36787  iss2  36878  ifp1bi  41896  prprelprb  45829  prprspr2  45830  eliunxp2  46529