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  6363  fununi  6604  fnopabg  6665  eqfnfv3  7020  respreima  7054  fsn  7125  brtpos2  8228  tpostpos  8242  oeeu  8591  mapval2  8879  xrltlen  13230  ssfzoulel  13849  xpcogend  15080  dfgcd2  16669  isffth2  18040  resscntz  19494  fiidomfld  20979  1stcelcls  23727  txflf  24272  fclsrest  24290  tsmssubm  24409  blres  24697  xrtgioo  25073  isncvsngp  25417  itg1climres  25982  ellimc3  26146  lgsquadlem1  27656  lgsquadlem2  27657  wlkson  30154  0clwlk  30640  dmrab  33012  qusker  33829  bnj594  35462  kardexen  35750  satf0  36052  bj-elid6  38005  bj-imdirco  38025  wl-df4-3mintru2  38324  poimirlem4  38456  rabeqel  39103  iss2  39190  ifp1bi  44440  prprelprb  48515  prprspr2  48516  dfsclnbgr6  48872  dfidom2  49356  eliunxp2  49362