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  2570  elon2  6405  fununi  6652  fnopabg  6716  eqfnfv3  7064  respreima  7097  fsn  7167  brtpos2  8269  tpostpos  8283  oeeu  8655  mapval2  8926  xrltlen  13204  ssfzoulel  13806  xpcogend  15019  dfgcd2  16587  isffth2  17978  resscntz  19368  fiidomfld  20792  1stcelcls  23483  txflf  24028  fclsrest  24046  tsmssubm  24165  blres  24455  xrtgioo  24840  isncvsngp  25195  itg1climres  25762  ellimc3  25926  lgsquadlem1  27433  lgsquadlem2  27434  wlkson  29683  0clwlk  30153  dmrab  32516  qusker  33334  bnj594  34880  satf0  35332  bj-elid6  37084  bj-imdirco  37104  wl-df4-3mintru2  37401  poimirlem4  37532  rabeqel  38158  iss2  38248  ifp1bi  43404  prprelprb  47323  prprspr2  47324  dfsclnbgr6  47659  eliunxp2  47976
  Copyright terms: Public domain W3C validator