MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  biancomi Structured version   Visualization version   GIF version

Theorem biancomi 463
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
StepHypRef Expression
1 biancomi.1 . 2 (𝜑 ↔ (𝜒𝜓))
2 ancom 461 . 2 ((𝜓𝜒) ↔ (𝜒𝜓))
31, 2bitr4i 277 1 (𝜑 ↔ (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 396
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 206  df-an 397
This theorem is referenced by:  biantrur  531  rbaibr  538  pm4.71ri  561  anbi2ci  625  anbi1ci  626  anbi12ci  628  an12  643  an32  644  mpbiran2  708  eu6lem  2567  elon2  6372  fununi  6620  fnopabg  6684  eqfnfv3  7031  respreima  7064  fsn  7129  brtpos2  8213  tpostpos  8227  oeeu  8599  mapval2  8862  xrltlen  13121  ssfzoulel  13722  xpcogend  14917  dfgcd2  16484  isffth2  17863  resscntz  19191  fiidomfld  20919  1stcelcls  22956  txflf  23501  fclsrest  23519  tsmssubm  23638  blres  23928  xrtgioo  24313  isncvsngp  24657  itg1climres  25223  ellimc3  25387  lgsquadlem1  26872  lgsquadlem2  26873  wlkson  28902  0clwlk  29372  dmrab  31724  qusker  32452  bnj594  33911  satf0  34351  bj-elid6  36039  bj-imdirco  36059  wl-df4-3mintru2  36356  poimirlem4  36480  rabeqel  37110  iss2  37201  ifp1bi  42238  prprelprb  46171  prprspr2  46172  eliunxp2  46962
  Copyright terms: Public domain W3C validator