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 224 1 (𝜓 → (𝜒𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  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 208  df-an 397
This theorem is referenced by:  rbaibr  538  pm5.44  543  exmoeub  2658  ssnelpss  4085  brinxp  5623  copsex2ga  5673  canth  7100  riotaxfrd  7137  iscard  9392  kmlem14  9577  ltxrlt  10699  elioo5  12782  prmind2  16017  pcelnn  16194  isnirred  19379  isreg2  21913  comppfsc  22068  kqcldsat  22269  elmptrab  22363  itg2uba  24271  prmorcht  25682  adjeq  29639  lnopcnbd  29740  cvexchlem  30072  maprnin  30393  topfne  33599  ismblfin  34814  ftc1anclem5  34852  isdmn2  35214  cdlemefrs29pre00  37411  cdlemefrs29cpre1  37414  isdomn3  39682  elmapintab  39834  bits0ALTV  43721
  Copyright terms: Public domain W3C validator