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  2574  elon2  6329  fununi  6568  fnopabg  6630  eqfnfv3  6980  respreima  7013  fsn  7082  brtpos2  8176  tpostpos  8190  oeeu  8533  mapval2  8814  xrltlen  13064  ssfzoulel  13680  xpcogend  14901  dfgcd2  16477  isffth2  17846  resscntz  19266  fiidomfld  20711  1stcelcls  23409  txflf  23954  fclsrest  23972  tsmssubm  24091  blres  24379  xrtgioo  24755  isncvsngp  25109  itg1climres  25675  ellimc3  25840  lgsquadlem1  27351  lgsquadlem2  27352  wlkson  29732  0clwlk  30209  dmrab  32574  qusker  33432  bnj594  35070  satf0  35568  bj-elid6  37377  bj-imdirco  37397  wl-df4-3mintru2  37694  poimirlem4  37827  rabeqel  38460  iss2  38547  ifp1bi  43810  prprelprb  47830  prprspr2  47831  dfsclnbgr6  48171  eliunxp2  48647