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  2567  elon2  6345  fununi  6593  fnopabg  6657  eqfnfv3  7007  respreima  7040  fsn  7109  brtpos2  8213  tpostpos  8227  oeeu  8569  mapval2  8847  xrltlen  13112  ssfzoulel  13727  xpcogend  14946  dfgcd2  16522  isffth2  17886  resscntz  19271  fiidomfld  20689  1stcelcls  23354  txflf  23899  fclsrest  23917  tsmssubm  24036  blres  24325  xrtgioo  24701  isncvsngp  25055  itg1climres  25621  ellimc3  25786  lgsquadlem1  27297  lgsquadlem2  27298  wlkson  29590  0clwlk  30065  dmrab  32432  qusker  33326  bnj594  34908  satf0  35359  bj-elid6  37153  bj-imdirco  37173  wl-df4-3mintru2  37470  poimirlem4  37613  rabeqel  38238  iss2  38321  ifp1bi  43484  prprelprb  47508  prprspr2  47509  dfsclnbgr6  47848  eliunxp2  48312