Theorem biancomi 462

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

Syntax hints:   ↔ wb 206   ∧ wa 395

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  df-an 396

This theorem is referenced by:  biantrur  530  rbaibr  537  pm4.71ri  560  anbi2ci  626  anbi1ci  627  anbi12ci  630  an12  646  an32  647  mpbiran2  711  eu6lem  2573  elon2  6334  fununi  6573  fnopabg  6635  eqfnfv3  6985  respreima  7018  fsn  7088  brtpos2  8182  tpostpos  8196  oeeu  8539  mapval2  8820  xrltlen  13097  ssfzoulel  13715  xpcogend  14936  dfgcd2  16515  isffth2  17885  resscntz  19308  fiidomfld  20751  1stcelcls  23426  txflf  23971  fclsrest  23989  tsmssubm  24108  blres  24396  xrtgioo  24772  isncvsngp  25116  itg1climres  25681  ellimc3  25846  lgsquadlem1  27343  lgsquadlem2  27344  wlkson  29723  0clwlk  30200  dmrab  32566  qusker  33409  bnj594  35054  satf0  35554  bj-elid6  37484  bj-imdirco  37504  wl-df4-3mintru2  37803  poimirlem4  37945  rabeqel  38578  iss2  38665  ifp1bi  43929  prprelprb  47977  prprspr2  47978  dfsclnbgr6  48334  eliunxp2  48810