Theorem biancomi 468

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  biantrur  540  rbaibr  547  pm4.71ri  570  anbi2ci  637  anbi1ci  638  anbi12ci  641  an12  658  an32  659  mpbiran2  723  3anan32  1113  eu6lem  2600  elon2  6372  fununi  6612  fnopabg  6673  eqfnfv3  7028  respreima  7062  fsn  7132  brtpos2  8233  tpostpos  8247  oeeu  8594  mapval2  8882  xrltlen  13199  ssfzoulel  13818  xpcogend  15049  dfgcd2  16640  isffth2  18011  resscntz  19461  fiidomfld  20942  1stcelcls  23688  txflf  24233  fclsrest  24251  tsmssubm  24370  blres  24658  xrtgioo  25034  isncvsngp  25378  itg1climres  25943  ellimc3  26108  lgsquadlem1  27614  lgsquadlem2  27615  wlkson  30100  0clwlk  30586  dmrab  32958  qusker  33776  bnj594  35408  kardexen  35676  satf0  35938  bj-elid6  37909  bj-imdirco  37929  wl-df4-3mintru2  38228  poimirlem4  38360  rabeqel  38992  iss2  39079  ifp1bi  44329  prprelprb  48404  prprspr2  48405  dfsclnbgr6  48761  dfidom2  49245  eliunxp2  49251