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  8684  elpmg  8840  letri3  11304  mulsuble0b  12091  xrletri3  13138  qbtwnre  13183  iooneg  13453  invsym  17714  subsubc  17808  lsslss  20717  znleval  21330  restopn2  22902  elflim2  23689  ismet2  24060  mbfi1fseqlem4  25469  deg1ldg  25846  sincosq1sgn  26245  lgsquadlem3  27122  numclwwlkqhash  29896  rmounid  32003  dfrdg4  35228  bj-19.41t  35956  bj-0int  36286  orddif0suc  42321  dflim7  42326  naddsuc2  42446  mpbiran4d  47571
  Copyright terms: Public domain W3C validator