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  6338  fununi  6577  fnopabg  6639  eqfnfv3  6989  respreima  7022  fsn  7092  brtpos2  8186  tpostpos  8200  oeeu  8543  mapval2  8824  xrltlen  13074  ssfzoulel  13690  xpcogend  14911  dfgcd2  16487  isffth2  17856  resscntz  19279  fiidomfld  20724  1stcelcls  23422  txflf  23967  fclsrest  23985  tsmssubm  24104  blres  24392  xrtgioo  24768  isncvsngp  25122  itg1climres  25688  ellimc3  25853  lgsquadlem1  27364  lgsquadlem2  27365  wlkson  29746  0clwlk  30223  dmrab  32589  qusker  33448  bnj594  35094  satf0  35594  bj-elid6  37452  bj-imdirco  37472  wl-df4-3mintru2  37769  poimirlem4  37904  rabeqel  38537  iss2  38624  ifp1bi  43887  prprelprb  47906  prprspr2  47907  dfsclnbgr6  48247  eliunxp2  48723