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  2572  elon2  6363  fununi  6610  fnopabg  6674  eqfnfv3  7022  respreima  7055  fsn  7124  brtpos2  8229  tpostpos  8243  oeeu  8613  mapval2  8884  xrltlen  13160  ssfzoulel  13774  xpcogend  14991  dfgcd2  16563  isffth2  17929  resscntz  19314  fiidomfld  20732  1stcelcls  23397  txflf  23942  fclsrest  23960  tsmssubm  24079  blres  24368  xrtgioo  24744  isncvsngp  25099  itg1climres  25665  ellimc3  25830  lgsquadlem1  27341  lgsquadlem2  27342  wlkson  29582  0clwlk  30057  dmrab  32424  qusker  33310  bnj594  34889  satf0  35340  bj-elid6  37134  bj-imdirco  37154  wl-df4-3mintru2  37451  poimirlem4  37594  rabeqel  38218  iss2  38308  ifp1bi  43473  prprelprb  47479  prprspr2  47480  dfsclnbgr6  47819  eliunxp2  48257