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  2568  elon2  6317  fununi  6556  fnopabg  6618  eqfnfv3  6966  respreima  6999  fsn  7068  brtpos2  8162  tpostpos  8176  oeeu  8518  mapval2  8796  xrltlen  13045  ssfzoulel  13660  xpcogend  14881  dfgcd2  16457  isffth2  17825  resscntz  19245  fiidomfld  20689  1stcelcls  23376  txflf  23921  fclsrest  23939  tsmssubm  24058  blres  24346  xrtgioo  24722  isncvsngp  25076  itg1climres  25642  ellimc3  25807  lgsquadlem1  27318  lgsquadlem2  27319  wlkson  29633  0clwlk  30110  dmrab  32476  qusker  33314  bnj594  34924  satf0  35416  bj-elid6  37214  bj-imdirco  37234  wl-df4-3mintru2  37531  poimirlem4  37663  rabeqel  38290  iss2  38375  ifp1bi  43594  prprelprb  47616  prprspr2  47617  dfsclnbgr6  47957  eliunxp2  48433