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

Theorem baibr 537
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 536 . 2 (𝜓 → (𝜑𝜒))
32bicomd 222 1 (𝜓 → (𝜒𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396
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 397
This theorem is referenced by:  rbaibr  538  pm5.44  543  exmoeub  2574  ssnelpss  4110  brinxp  5752  copsex2ga  5805  canth  7358  riotaxfrd  7396  iscard  9966  kmlem14  10154  ltxrlt  11280  elioo5  13377  prmind2  16618  pcelnn  16799  isnirred  20226  isreg2  22872  comppfsc  23027  kqcldsat  23228  elmptrab  23322  itg2uba  25252  prmorcht  26671  adjeq  31175  lnopcnbd  31276  cvexchlem  31608  maprnin  31943  topfne  35227  ismblfin  36517  ftc1anclem5  36553  isdmn2  36911  cdlemefrs29pre00  39254  cdlemefrs29cpre1  39257  isdomn3  41931  elmapintab  42332  bits0ALTV  46333
  Copyright terms: Public domain W3C validator