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 223 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:  rbaibr  537  pm5.44  542  exmoeub  2580  ssnelpss  4114  brinxp  5764  copsex2ga  5817  canth  7385  riotaxfrd  7422  iscard  10015  kmlem14  10204  ltxrlt  11331  elioo5  13444  prmind2  16722  pcelnn  16908  isnirred  20420  isdomn3  20715  isreg2  23385  comppfsc  23540  kqcldsat  23741  elmptrab  23835  itg2uba  25778  prmorcht  27221  adjeq  31954  lnopcnbd  32055  cvexchlem  32387  maprnin  32742  topfne  36355  ismblfin  37668  ftc1anclem5  37704  isdmn2  38062  cdlemefrs29pre00  40397  cdlemefrs29cpre1  40400  elmapintab  43609  bits0ALTV  47666
  Copyright terms: Public domain W3C validator