Theorem biancomi 467

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

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

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 401

This theorem is used by:  biantrur  539  rbaibr  546  pm4.71ri  569  anbi2ci  636  anbi1ci  637  anbi12ci  640  an12  657  an32  658  mpbiran2  722  3anan32  1112  eu6lem  2600  elon2  6371  fununi  6611  fnopabg  6672  eqfnfv3  7027  respreima  7061  fsn  7131  brtpos2  8226  tpostpos  8240  oeeu  8587  mapval2  8868  xrltlen  13177  ssfzoulel  13796  xpcogend  15018  dfgcd2  16610  isffth2  17981  resscntz  19409  fiidomfld  20889  1stcelcls  23629  txflf  24174  fclsrest  24192  tsmssubm  24311  blres  24599  xrtgioo  24975  isncvsngp  25319  itg1climres  25884  ellimc3  26049  lgsquadlem1  27555  lgsquadlem2  27556  wlkson  30015  0clwlk  30492  dmrab  32854  qusker  33678  bnj594  35309  kardexen  35584  satf0  35872  bj-elid6  37842  bj-imdirco  37862  wl-df4-3mintru2  38161  poimirlem4  38303  rabeqel  38934  iss2  39021  ifp1bi  44256  prprelprb  48294  prprspr2  48295  dfsclnbgr6  48651  dfidom2  49136  eliunxp2  49142