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  6318  fununi  6557  fnopabg  6619  eqfnfv3  6967  respreima  7000  fsn  7069  brtpos2  8165  tpostpos  8179  oeeu  8521  mapval2  8799  xrltlen  13048  ssfzoulel  13663  xpcogend  14881  dfgcd2  16457  isffth2  17825  resscntz  19212  fiidomfld  20659  1stcelcls  23346  txflf  23891  fclsrest  23909  tsmssubm  24028  blres  24317  xrtgioo  24693  isncvsngp  25047  itg1climres  25613  ellimc3  25778  lgsquadlem1  27289  lgsquadlem2  27290  wlkson  29600  0clwlk  30074  dmrab  32441  qusker  33287  bnj594  34885  satf0  35355  bj-elid6  37154  bj-imdirco  37174  wl-df4-3mintru2  37471  poimirlem4  37614  rabeqel  38239  iss2  38322  ifp1bi  43485  prprelprb  47511  prprspr2  47512  dfsclnbgr6  47852  eliunxp2  48328