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

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
StepHypRef Expression
1 biancomi.1 . 2 (𝜑 ↔ (𝜒𝜓))
2 ancom 460 . 2 ((𝜓𝜒) ↔ (𝜒𝜓))
31, 2bitr4i 278 1 (𝜑 ↔ (𝜓𝜒))
Colors of variables: wff setvar class
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  624  anbi1ci  625  anbi12ci  628  an12  644  an32  645  mpbiran2  709  eu6lem  2576  elon2  6406  fununi  6653  fnopabg  6717  eqfnfv3  7066  respreima  7099  fsn  7169  brtpos2  8273  tpostpos  8287  oeeu  8659  mapval2  8930  xrltlen  13208  ssfzoulel  13810  xpcogend  15023  dfgcd2  16593  isffth2  17983  resscntz  19373  fiidomfld  20797  1stcelcls  23490  txflf  24035  fclsrest  24053  tsmssubm  24172  blres  24462  xrtgioo  24847  isncvsngp  25202  itg1climres  25769  ellimc3  25934  lgsquadlem1  27442  lgsquadlem2  27443  wlkson  29692  0clwlk  30162  dmrab  32525  qusker  33342  bnj594  34888  satf0  35340  bj-elid6  37136  bj-imdirco  37156  wl-df4-3mintru2  37453  poimirlem4  37584  rabeqel  38210  iss2  38300  ifp1bi  43464  prprelprb  47391  prprspr2  47392  dfsclnbgr6  47730  eliunxp2  48058
  Copyright terms: Public domain W3C validator