Theorem biancomi 455

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 453	. 2 ⊢ ((𝜓 ∧ 𝜒) ↔ (𝜒 ∧ 𝜓))
3	1, 2	bitr4i 270	1 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))

Syntax hints:   ↔ wb 198   ∧ wa 387

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 199  df-an 388

This theorem is referenced by:  anbi2ci  616  anbi1ci  617  anbi12ci  619  eu6lem  2593  elon2  6045  fununi  6267  fnopabg  6320  eqfnfv3  6635  respreima  6667  fsn  6726  brtpos2  7707  tpostpos  7721  oeeu  8036  mapval2  8242  xrltlen  12362  ssfzoulel  12952  xpcogend  14201  dfgcd2  15756  isffth2  17056  resscntz  18245  fiidomfld  19814  1stcelcls  21788  txflf  22333  fclsrest  22351  tsmssubm  22469  blres  22759  xrtgioo  23132  isncvsngp  23471  itg1climres  24033  ellimc3  24195  lgsquadlem1  25673  lgsquadlem2  25674  wlkson  27155  0clwlk  27674  dmrab  30054  qusker  30629  bnj594  31863  satf0  32222  rabeqel  35000  iss2  35087  prprelprb  43082  prprspr2  43083  eliunxp2  43781