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

Theorem baibr 965
 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 964 . 2 (𝜓 → (𝜑𝜒))
32bicomd 213 1 (𝜓 → (𝜒𝜑))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383 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 385 This theorem is referenced by:  pm5.44  970  exmoeu2  2525  ssnelpss  3751  brinxp  5215  copsex2ga  5264  canth  6648  riotaxfrd  6682  iscard  8839  kmlem14  9023  ltxrlt  10146  elioo5  12269  prmind2  15445  pcelnn  15621  isnirred  18746  isreg2  21229  comppfsc  21383  kqcldsat  21584  elmptrab  21678  itg2uba  23555  prmorcht  24949  adjeq  28922  lnopcnbd  29023  cvexchlem  29355  maprnin  29634  topfne  32474  ismblfin  33580  ftc1anclem5  33619  isdmn2  33984  cdlemefrs29pre00  36000  cdlemefrs29cpre1  36003  isdomn3  38099  elmapintab  38219  bits0ALTV  41915
 Copyright terms: Public domain W3C validator