Theorem biancomi 464

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

Syntax hints:   ↔ wb 205   ∧ wa 397

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 398

This theorem is referenced by:  biantrur  532  rbaibr  539  pm4.71ri  562  anbi2ci  626  anbi1ci  627  anbi12ci  629  an12  643  an32  644  mpbiran2  708  eu6lem  2571  elon2  6292  fununi  6538  fnopabg  6600  eqfnfv3  6943  respreima  6975  fsn  7039  brtpos2  8079  tpostpos  8093  oeeu  8465  mapval2  8691  xrltlen  12930  ssfzoulel  13531  xpcogend  14734  dfgcd2  16303  isffth2  17681  resscntz  18987  fiidomfld  20629  1stcelcls  22661  txflf  23206  fclsrest  23224  tsmssubm  23343  blres  23633  xrtgioo  24018  isncvsngp  24362  itg1climres  24928  ellimc3  25092  lgsquadlem1  26577  lgsquadlem2  26578  wlkson  28073  0clwlk  28543  dmrab  30893  qusker  31598  bnj594  32941  satf0  33383  bj-elid6  35389  bj-imdirco  35409  wl-df4-3mintru2  35706  poimirlem4  35829  rabeqel  36464  iss2  36557  ifp1bi  41322  prprelprb  45213  prprspr2  45214  eliunxp2  45913