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  644  an32  645  mpbiran2  709  eu6lem  2568  elon2  6376  fununi  6624  fnopabg  6688  eqfnfv3  7035  respreima  7068  fsn  7133  brtpos2  8217  tpostpos  8231  oeeu  8603  mapval2  8866  xrltlen  13125  ssfzoulel  13726  xpcogend  14921  dfgcd2  16488  isffth2  17867  resscntz  19197  fiidomfld  20927  1stcelcls  22965  txflf  23510  fclsrest  23528  tsmssubm  23647  blres  23937  xrtgioo  24322  isncvsngp  24666  itg1climres  25232  ellimc3  25396  lgsquadlem1  26883  lgsquadlem2  26884  wlkson  28913  0clwlk  29383  dmrab  31737  qusker  32464  bnj594  33923  satf0  34363  bj-elid6  36051  bj-imdirco  36071  wl-df4-3mintru2  36368  poimirlem4  36492  rabeqel  37122  iss2  37213  ifp1bi  42253  prprelprb  46185  prprspr2  46186  eliunxp2  47009