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  626  anbi1ci  627  anbi12ci  630  an12  646  an32  647  mpbiran2  711  eu6lem  2572  elon2  6327  fununi  6566  fnopabg  6628  eqfnfv3  6978  respreima  7011  fsn  7080  brtpos2  8174  tpostpos  8188  oeeu  8531  mapval2  8812  xrltlen  13062  ssfzoulel  13678  xpcogend  14899  dfgcd2  16475  isffth2  17844  resscntz  19264  fiidomfld  20709  1stcelcls  23407  txflf  23952  fclsrest  23970  tsmssubm  24089  blres  24377  xrtgioo  24753  isncvsngp  25107  itg1climres  25673  ellimc3  25838  lgsquadlem1  27349  lgsquadlem2  27350  wlkson  29709  0clwlk  30186  dmrab  32551  qusker  33409  bnj594  35047  satf0  35545  bj-elid6  37344  bj-imdirco  37364  wl-df4-3mintru2  37661  poimirlem4  37794  rabeqel  38426  iss2  38514  ifp1bi  43780  prprelprb  47800  prprspr2  47801  dfsclnbgr6  48141  eliunxp2  48617