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  6330  fununi  6569  fnopabg  6631  eqfnfv3  6981  respreima  7014  fsn  7084  brtpos2  8177  tpostpos  8191  oeeu  8534  mapval2  8815  xrltlen  13092  ssfzoulel  13710  xpcogend  14931  dfgcd2  16510  isffth2  17880  resscntz  19303  fiidomfld  20746  1stcelcls  23440  txflf  23985  fclsrest  24003  tsmssubm  24122  blres  24410  xrtgioo  24786  isncvsngp  25130  itg1climres  25695  ellimc3  25860  lgsquadlem1  27361  lgsquadlem2  27362  wlkson  29742  0clwlk  30219  dmrab  32585  qusker  33428  bnj594  35074  satf0  35574  bj-elid6  37504  bj-imdirco  37524  wl-df4-3mintru2  37823  poimirlem4  37965  rabeqel  38598  iss2  38685  ifp1bi  43953  prprelprb  47995  prprspr2  47996  dfsclnbgr6  48352  eliunxp2  48828