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

This theorem is referenced by:  biantrur  530  rbaibr  537  pm4.71ri  560  anbi2ci  625  anbi1ci  626  anbi12ci  629  an12  645  an32  646  mpbiran2  710  eu6lem  2566  elon2  6331  fununi  6575  fnopabg  6637  eqfnfv3  6987  respreima  7020  fsn  7089  brtpos2  8188  tpostpos  8202  oeeu  8544  mapval2  8822  xrltlen  13082  ssfzoulel  13697  xpcogend  14916  dfgcd2  16492  isffth2  17860  resscntz  19247  fiidomfld  20694  1stcelcls  23381  txflf  23926  fclsrest  23944  tsmssubm  24063  blres  24352  xrtgioo  24728  isncvsngp  25082  itg1climres  25648  ellimc3  25813  lgsquadlem1  27324  lgsquadlem2  27325  wlkson  29635  0clwlk  30109  dmrab  32476  qusker  33313  bnj594  34895  satf0  35352  bj-elid6  37151  bj-imdirco  37171  wl-df4-3mintru2  37468  poimirlem4  37611  rabeqel  38236  iss2  38319  ifp1bi  43484  prprelprb  47511  prprspr2  47512  dfsclnbgr6  47851  eliunxp2  48315