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  2567  elon2  6372  fununi  6620  fnopabg  6684  eqfnfv3  7031  respreima  7064  fsn  7129  brtpos2  8213  tpostpos  8227  oeeu  8599  mapval2  8862  xrltlen  13121  ssfzoulel  13722  xpcogend  14917  dfgcd2  16484  isffth2  17863  resscntz  19191  fiidomfld  20919  1stcelcls  22956  txflf  23501  fclsrest  23519  tsmssubm  23638  blres  23928  xrtgioo  24313  isncvsngp  24657  itg1climres  25223  ellimc3  25387  lgsquadlem1  26872  lgsquadlem2  26873  wlkson  28902  0clwlk  29372  dmrab  31724  qusker  32452  bnj594  33911  satf0  34351  bj-elid6  36039  bj-imdirco  36059  wl-df4-3mintru2  36356  poimirlem4  36480  rabeqel  37110  iss2  37201  ifp1bi  42238  prprelprb  46171  prprspr2  46172  eliunxp2  46962