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 277	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  641  an32  642  mpbiran2  706  eu6lem  2574  elon2  6274  fununi  6505  fnopabg  6566  eqfnfv3  6905  respreima  6937  fsn  7001  brtpos2  8032  tpostpos  8046  oeeu  8410  mapval2  8634  xrltlen  12862  ssfzoulel  13462  xpcogend  14666  dfgcd2  16235  isffth2  17613  resscntz  18919  fiidomfld  20561  1stcelcls  22593  txflf  23138  fclsrest  23156  tsmssubm  23275  blres  23565  xrtgioo  23950  isncvsngp  24294  itg1climres  24860  ellimc3  25024  lgsquadlem1  26509  lgsquadlem2  26510  wlkson  28004  0clwlk  28473  dmrab  30823  qusker  31528  bnj594  32871  satf0  33313  bj-elid6  35320  bj-imdirco  35340  wl-df4-3mintru2  35637  poimirlem4  35760  rabeqel  36373  iss2  36458  ifp1bi  41071  prprelprb  44921  prprspr2  44922  eliunxp2  45621