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  2601  elon2  6388  fununi  6634  fnopabg  6695  eqfnfv3  7051  respreima  7086  fsn  7157  brtpos2  8274  tpostpos  8288  oeeu  8637  mapval2  8925  xrltlen  13299  ssfzoulel  13919  xpcogend  15153  dfgcd2  16745  isffth2  18119  resscntz  19574  fiidomfld  21059  1stcelcls  23807  txflf  24352  fclsrest  24370  tsmssubm  24489  blres  24777  xrtgioo  25153  isncvsngp  25497  itg1climres  26062  ellimc3  26226  lgsquadlem1  27734  lgsquadlem2  27735  wlkson  30262  0clwlk  30748  dmrab  33162  qusker  33977  bnj594  35609  kardexen  35930  satf0  36303  mirimanofffr  36628  bj-elinxp  38137  bj-elid6  38282  bj-imdirco  38302  wl-df4-3mintru2  38601  poimirlem4  38733  rabeqel  39380  iss2  39467  ifp1bi  44693  prprelprb  48802  prprspr2  48803  dfsclnbgr6  49159  dfidom2  49643  eliunxp2  49649