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

Theorem biancomd 463
Description: Commuting conjunction in a biconditional, deduction form. (Contributed by Peter Mazsa, 3-Oct-2018.)
Hypothesis
Ref Expression
biancomd.1 (𝜑 → (𝜓 ↔ (𝜃𝜒)))
Assertion
Ref Expression
biancomd (𝜑 → (𝜓 ↔ (𝜒𝜃)))

Proof of Theorem biancomd
StepHypRef Expression
1 biancomd.1 . 2 (𝜑 → (𝜓 ↔ (𝜃𝜒)))
2 ancom 460 . 2 ((𝜃𝜒) ↔ (𝜒𝜃))
31, 2bitrdi 287 1 (𝜑 → (𝜓 ↔ (𝜒𝜃)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  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 206  df-an 396
This theorem is referenced by:  ibar  528  rbaibd  540  pm4.71rd  562  anbi1cd  633  mpbiran2d  705  naddcom  8687  elpmg  8843  letri3  11306  mulsuble0b  12093  xrletri3  13140  qbtwnre  13185  iooneg  13455  invsym  17716  subsubc  17810  lsslss  20720  znleval  21333  restopn2  22914  elflim2  23701  ismet2  24072  mbfi1fseqlem4  25481  deg1ldg  25859  sincosq1sgn  26259  lgsquadlem3  27136  numclwwlkqhash  29910  rmounid  32017  dfrdg4  35242  bj-19.41t  35968  bj-0int  36298  orddif0suc  42333  dflim7  42338  naddsuc2  42458  mpbiran4d  47583
  Copyright terms: Public domain W3C validator