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  6326  fununi  6565  fnopabg  6627  eqfnfv3  6977  respreima  7010  fsn  7080  brtpos2  8173  tpostpos  8187  oeeu  8530  mapval2  8811  xrltlen  13086  ssfzoulel  13704  xpcogend  14925  dfgcd2  16504  isffth2  17874  resscntz  19297  fiidomfld  20740  1stcelcls  23435  txflf  23980  fclsrest  23998  tsmssubm  24117  blres  24405  xrtgioo  24781  isncvsngp  25125  itg1climres  25690  ellimc3  25855  lgsquadlem1  27362  lgsquadlem2  27363  wlkson  29743  0clwlk  30220  dmrab  32586  qusker  33429  bnj594  35075  satf0  35575  bj-elid6  37497  bj-imdirco  37517  wl-df4-3mintru2  37814  poimirlem4  37956  rabeqel  38589  iss2  38676  ifp1bi  43944  prprelprb  47974  prprspr2  47975  dfsclnbgr6  48331  eliunxp2  48807