Theorem biancomi 462

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

Syntax hints:   ↔ wb 205   ∧ wa 395

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 206  df-an 396

This theorem is referenced by:  biantrur  530  rbaibr  537  pm4.71ri  560  anbi2ci  624  anbi1ci  625  anbi12ci  627  an12  644  an32  645  mpbiran2  709  eu6lem  2562  elon2  6374  fununi  6622  fnopabg  6686  eqfnfv3  7036  respreima  7069  fsn  7138  brtpos2  8231  tpostpos  8245  oeeu  8617  mapval2  8882  xrltlen  13149  ssfzoulel  13750  xpcogend  14945  dfgcd2  16513  isffth2  17896  resscntz  19275  fiidomfld  21249  1stcelcls  23352  txflf  23897  fclsrest  23915  tsmssubm  24034  blres  24324  xrtgioo  24709  isncvsngp  25064  itg1climres  25631  ellimc3  25795  lgsquadlem1  27300  lgsquadlem2  27301  wlkson  29457  0clwlk  29927  dmrab  32281  qusker  33001  bnj594  34479  satf0  34918  bj-elid6  36585  bj-imdirco  36605  wl-df4-3mintru2  36902  poimirlem4  37032  rabeqel  37661  iss2  37752  ifp1bi  42855  prprelprb  46780  prprspr2  46781  eliunxp2  47320