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  2571  elon2  6376  fununi  6622  fnopabg  6686  eqfnfv3  7034  respreima  7067  fsn  7136  brtpos2  8240  tpostpos  8254  oeeu  8624  mapval2  8895  xrltlen  13171  ssfzoulel  13782  xpcogend  14996  dfgcd2  16566  isffth2  17939  resscntz  19325  fiidomfld  20748  1stcelcls  23434  txflf  23979  fclsrest  23997  tsmssubm  24116  blres  24405  xrtgioo  24783  isncvsngp  25138  itg1climres  25704  ellimc3  25869  lgsquadlem1  27379  lgsquadlem2  27380  wlkson  29621  0clwlk  30096  dmrab  32463  qusker  33318  bnj594  34867  satf0  35318  bj-elid6  37112  bj-imdirco  37132  wl-df4-3mintru2  37429  poimirlem4  37572  rabeqel  38196  iss2  38286  ifp1bi  43460  prprelprb  47450  prprspr2  47451  dfsclnbgr6  47790  eliunxp2  48196