Theorem biancomi 466

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

Syntax hints:   ↔ wb 209   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  biantrur  534  rbaibr  541  pm4.71ri  564  anbi2ci  628  anbi1ci  629  anbi12ci  631  an12  645  an32  646  mpbiran2  710  eu6lem  2572  elon2  6202  fununi  6433  fnopabg  6493  eqfnfv3  6832  respreima  6864  fsn  6928  brtpos2  7952  tpostpos  7966  oeeu  8309  mapval2  8531  xrltlen  12701  ssfzoulel  13301  xpcogend  14502  dfgcd2  16069  isffth2  17377  resscntz  18680  fiidomfld  20300  1stcelcls  22312  txflf  22857  fclsrest  22875  tsmssubm  22994  blres  23283  xrtgioo  23657  isncvsngp  24000  itg1climres  24566  ellimc3  24730  lgsquadlem1  26215  lgsquadlem2  26216  wlkson  27698  0clwlk  28167  dmrab  30517  qusker  31217  bnj594  32559  satf0  33001  bj-elid6  35025  bj-imdirco  35045  wl-df4-3mintru2  35344  poimirlem4  35467  rabeqel  36080  iss2  36165  ifp1bi  40735  prprelprb  44585  prprspr2  44586  eliunxp2  45285