Theorem biancomi 466

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

Syntax hints:   ↔ wb 208   ∧ wa 399

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 400

This theorem is referenced by:  biantrur  538  rbaibr  545  pm4.71ri  568  anbi2ci  634  anbi1ci  635  anbi12ci  638  an12  655  an32  656  mpbiran2  720  3anan32  1109  eu6lem  2602  elon2  6359  fununi  6598  fnopabg  6660  eqfnfv3  7015  respreima  7049  fsn  7119  brtpos2  8214  tpostpos  8228  oeeu  8575  mapval2  8856  xrltlen  13150  ssfzoulel  13768  xpcogend  14989  dfgcd2  16582  isffth2  17953  resscntz  19375  fiidomfld  20826  1stcelcls  23523  txflf  24068  fclsrest  24086  tsmssubm  24205  blres  24493  xrtgioo  24869  isncvsngp  25213  itg1climres  25778  ellimc3  25943  lgsquadlem1  27446  lgsquadlem2  27447  wlkson  29857  0clwlk  30334  dmrab  32698  qusker  33537  bnj594  35209  satf0  35727  bj-elid6  37667  bj-imdirco  37687  wl-df4-3mintru2  37986  poimirlem4  38128  rabeqel  38761  iss2  38848  ifp1bi  44083  prprelprb  48128  prprspr2  48129  dfsclnbgr6  48485  eliunxp2  48961