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

Theorem baibr 944
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 943 . 2 (𝜓 → (𝜑𝜒))
32bicomd 213 1 (𝜓 → (𝜒𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384
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 197  df-an 386
This theorem is referenced by:  pm5.44  949  exmoeu2  2501  ssnelpss  3701  brinxp  5147  copsex2ga  5197  canth  6563  riotaxfrd  6597  iscard  8746  kmlem14  8930  ltxrlt  10053  elioo5  12170  prmind2  15317  pcelnn  15493  isnirred  18616  isreg2  21086  comppfsc  21240  kqcldsat  21441  elmptrab  21535  itg2uba  23411  prmorcht  24799  adjeq  28634  lnopcnbd  28735  cvexchlem  29067  maprnin  29340  topfne  31983  ismblfin  33068  ftc1anclem5  33107  isdmn2  33472  cdlemefrs29pre00  35149  cdlemefrs29cpre1  35152  isdomn3  37249  elmapintab  37369  bits0ALTV  40877
  Copyright terms: Public domain W3C validator