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  2571  elon2  6397  fununi  6643  fnopabg  6706  eqfnfv3  7053  respreima  7086  fsn  7155  brtpos2  8256  tpostpos  8270  oeeu  8640  mapval2  8911  xrltlen  13185  ssfzoulel  13796  xpcogend  15010  dfgcd2  16580  isffth2  17970  resscntz  19364  fiidomfld  20792  1stcelcls  23485  txflf  24030  fclsrest  24048  tsmssubm  24167  blres  24457  xrtgioo  24842  isncvsngp  25197  itg1climres  25764  ellimc3  25929  lgsquadlem1  27439  lgsquadlem2  27440  wlkson  29689  0clwlk  30159  dmrab  32525  qusker  33357  bnj594  34905  satf0  35357  bj-elid6  37153  bj-imdirco  37173  wl-df4-3mintru2  37470  poimirlem4  37611  rabeqel  38236  iss2  38326  ifp1bi  43492  prprelprb  47442  prprspr2  47443  dfsclnbgr6  47782  eliunxp2  48179