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  707  naddcom  8696  elpmg  8853  letri3  11321  mulsuble0b  12108  xrletri3  13157  qbtwnre  13202  iooneg  13472  invsym  17736  subsubc  17830  lsslss  20834  znleval  21475  restopn2  23068  elflim2  23855  ismet2  24226  mbfi1fseqlem4  25635  deg1ldg  26015  sincosq1sgn  26420  lgsquadlem3  27302  renegscl  28213  numclwwlkqhash  30172  rmounid  32279  dfrdg4  35483  bj-19.41t  36187  bj-0int  36516  orddif0suc  42620  dflim7  42625  naddsuc2  42745  mpbiran4d  47793
  Copyright terms: Public domain W3C validator