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

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
StepHypRef Expression
1 biancomi.1 . 2 (𝜑 ↔ (𝜒𝜓))
2 ancom 453 . 2 ((𝜓𝜒) ↔ (𝜒𝜓))
31, 2bitr4i 270 1 (𝜑 ↔ (𝜓𝜒))
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator