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

Theorem biancomi 466
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 464 . 2 ((𝜓𝜒) ↔ (𝜒𝜓))
31, 2bitr4i 281 1 (𝜑 ↔ (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wb 209  wa 399
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 210  df-an 400
This theorem is referenced by:  biantrur  534  rbaibr  541  pm4.71ri  564  anbi2ci  627  anbi1ci  628  anbi12ci  630  an12  644  an32  645  mpbiran2  709  eu6lem  2636  elon2  6174  fununi  6403  fnopabg  6461  eqfnfv3  6785  respreima  6817  fsn  6878  brtpos2  7885  tpostpos  7899  oeeu  8216  mapval2  8423  xrltlen  12531  ssfzoulel  13130  xpcogend  14329  dfgcd2  15887  isffth2  17181  resscntz  18457  fiidomfld  20077  1stcelcls  22069  txflf  22614  fclsrest  22632  tsmssubm  22751  blres  23041  xrtgioo  23414  isncvsngp  23757  itg1climres  24321  ellimc3  24485  lgsquadlem1  25967  lgsquadlem2  25968  wlkson  27449  0clwlk  27918  dmrab  30270  qusker  30972  bnj594  32292  satf0  32727  bj-elid6  34580  bj-imdirco  34600  wl-df4-3mintru2  34897  rabeqel  35669  iss2  35754  ifp1bi  40197  prprelprb  44021  prprspr2  44022  eliunxp2  44722
  Copyright terms: Public domain W3C validator