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  2573  elon2  6368  fununi  6616  fnopabg  6680  eqfnfv3  7028  respreima  7061  fsn  7130  brtpos2  8236  tpostpos  8250  oeeu  8620  mapval2  8891  xrltlen  13167  ssfzoulel  13781  xpcogend  14998  dfgcd2  16570  isffth2  17936  resscntz  19321  fiidomfld  20739  1stcelcls  23404  txflf  23949  fclsrest  23967  tsmssubm  24086  blres  24375  xrtgioo  24751  isncvsngp  25106  itg1climres  25672  ellimc3  25837  lgsquadlem1  27348  lgsquadlem2  27349  wlkson  29641  0clwlk  30116  dmrab  32483  qusker  33369  bnj594  34948  satf0  35399  bj-elid6  37193  bj-imdirco  37213  wl-df4-3mintru2  37510  poimirlem4  37653  rabeqel  38277  iss2  38367  ifp1bi  43501  prprelprb  47511  prprspr2  47512  dfsclnbgr6  47851  eliunxp2  48289