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

Theorem baibr 536
Description: Move conjunction outside of biconditional. (Contributed by NM, 11-Jul-1994.)
Hypothesis
Ref Expression
baib.1 (𝜑 ↔ (𝜓𝜒))
Assertion
Ref Expression
baibr (𝜓 → (𝜒𝜑))

Proof of Theorem baibr
StepHypRef Expression
1 baib.1 . . 3 (𝜑 ↔ (𝜓𝜒))
21baib 535 . 2 (𝜓 → (𝜑𝜒))
32bicomd 222 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:  rbaibr  537  pm5.44  542  exmoeub  2566  ssnelpss  4103  brinxp  5744  copsex2ga  5797  canth  7354  riotaxfrd  7392  iscard  9966  kmlem14  10154  ltxrlt  11281  elioo5  13378  prmind2  16619  pcelnn  16802  isnirred  20312  isreg2  23203  comppfsc  23358  kqcldsat  23559  elmptrab  23653  itg2uba  25595  prmorcht  27026  adjeq  31657  lnopcnbd  31758  cvexchlem  32090  maprnin  32425  topfne  35729  ismblfin  37019  ftc1anclem5  37055  isdmn2  37413  cdlemefrs29pre00  39756  cdlemefrs29cpre1  39759  isdomn3  42435  elmapintab  42836  bits0ALTV  46832
  Copyright terms: Public domain W3C validator