Theorem biancomi 465

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

Syntax hints:   ↔ wb 208   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  biantrur  533  rbaibr  540  pm4.71ri  563  anbi2ci  626  anbi1ci  627  anbi12ci  629  an12  643  an32  644  mpbiran2  708  eu6lem  2658  elon2  6202  fununi  6429  fnopabg  6485  eqfnfv3  6804  respreima  6836  fsn  6897  brtpos2  7898  tpostpos  7912  oeeu  8229  mapval2  8436  xrltlen  12540  ssfzoulel  13132  xpcogend  14334  dfgcd2  15894  isffth2  17186  resscntz  18462  fiidomfld  20081  1stcelcls  22069  txflf  22614  fclsrest  22632  tsmssubm  22751  blres  23041  xrtgioo  23414  isncvsngp  23753  itg1climres  24315  ellimc3  24477  lgsquadlem1  25956  lgsquadlem2  25957  wlkson  27438  0clwlk  27909  dmrab  30260  qusker  30918  bnj594  32184  satf0  32619  bj-elid6  34465  rabeqel  35531  iss2  35616  ifp1bi  39888  prprelprb  43699  prprspr2  43700  eliunxp2  44402