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  2598  elon2  6373  fununi  6615  fnopabg  6676  eqfnfv3  7031  respreima  7065  fsn  7136  brtpos2  8249  tpostpos  8263  oeeu  8612  mapval2  8900  xrltlen  13275  ssfzoulel  13895  xpcogend  15127  dfgcd2  16719  isffth2  18093  resscntz  19547  fiidomfld  21032  1stcelcls  23780  txflf  24325  fclsrest  24343  tsmssubm  24462  blres  24750  xrtgioo  25126  isncvsngp  25470  itg1climres  26035  ellimc3  26199  lgsquadlem1  27707  lgsquadlem2  27708  wlkson  30235  0clwlk  30721  dmrab  33093  qusker  33910  bnj594  35542  kardexen  35831  satf0  36137  coi1in  37961  bj-elid6  38092  bj-imdirco  38112  wl-df4-3mintru2  38411  poimirlem4  38543  rabeqel  39190  iss2  39277  ifp1bi  44503  prprelprb  48599  prprspr2  48600  dfsclnbgr6  48956  dfidom2  49440  eliunxp2  49446