Theorem biancomi 464

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

Syntax hints:   ↔ wb 208   ∧ wa 397

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 209  df-an 398

This theorem is referenced by:  biantrur  536  rbaibr  543  pm4.71ri  566  anbi2ci  632  anbi1ci  633  anbi12ci  636  an12  652  an32  653  mpbiran2  717  eu6lem  2579  elon2  6325  fununi  6564  fnopabg  6626  eqfnfv3  6977  respreima  7011  fsn  7081  brtpos2  8176  tpostpos  8190  oeeu  8533  mapval2  8814  xrltlen  13092  ssfzoulel  13710  xpcogend  14931  dfgcd2  16510  isffth2  17880  resscntz  19303  fiidomfld  20750  1stcelcls  23448  txflf  23993  fclsrest  24011  tsmssubm  24130  blres  24418  xrtgioo  24794  isncvsngp  25138  itg1climres  25703  ellimc3  25868  lgsquadlem1  27365  lgsquadlem2  27366  wlkson  29745  0clwlk  30222  dmrab  32588  qusker  33436  bnj594  35109  satf0  35615  bj-elid6  37545  bj-imdirco  37565  wl-df4-3mintru2  37864  poimirlem4  38006  rabeqel  38639  iss2  38726  ifp1bi  43961  prprelprb  48006  prprspr2  48007  dfsclnbgr6  48363  eliunxp2  48839