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

Theorem biancomd 466
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 463 . 2 ((𝜃𝜒) ↔ (𝜒𝜃))
31, 2syl6bb 289 1 (𝜑 → (𝜓 ↔ (𝜒𝜃)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 208  wa 398
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 209  df-an 399
This theorem is referenced by:  ibar  531  rbaibd  543  pm4.71rd  565  anbi1cd  635  mpbiran2d  706  elpmg  8414  letri3  10718  mulsuble0b  11504  xrletri3  12539  qbtwnre  12584  iooneg  12849  invsym  17024  subsubc  17115  lsslss  19725  znleval  20693  restopn2  21777  elflim2  22564  ismet2  22935  mbfi1fseqlem4  24311  deg1ldg  24678  sincosq1sgn  25076  lgsquadlem3  25950  numclwwlkqhash  28146  rmounid  30251  dfrdg4  33405  bj-19.41t  34096  bj-0int  34385
  Copyright terms: Public domain W3C validator