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 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:  ibar  528  rbaibd  540  pm4.71rd  562  anbi1cd  635  mpbiran2d  708  naddcom  8719  naddsuc2  8738  elpmg  8882  letri3  11344  mulsuble0b  12138  xrletri3  13193  qbtwnre  13238  iooneg  13508  invsym  17810  subsubc  17904  lsslss  20977  znleval  21591  restopn2  23201  elflim2  23988  ismet2  24359  mbfi1fseqlem4  25768  deg1ldg  26146  sincosq1sgn  26555  lgsquadlem3  27441  renegscl  28445  numclwwlkqhash  30404  rmounid  32523  dfrdg4  35933  bj-19.41t  36757  bj-0int  37084  orddif0suc  43258  dflim7  43263  mpbiran4d  48647
  Copyright terms: Public domain W3C validator