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

Theorem baibr 540
 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 539 . 2 (𝜓 → (𝜑𝜒))
32bicomd 226 1 (𝜓 → (𝜒𝜑))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399 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 210  df-an 400 This theorem is referenced by:  rbaibr  541  pm5.44  546  exmoeub  2640  ssnelpss  4039  brinxp  5595  copsex2ga  5645  canth  7091  riotaxfrd  7128  iscard  9391  kmlem14  9577  ltxrlt  10703  elioo5  12785  prmind2  16022  pcelnn  16199  isnirred  19450  isreg2  21992  comppfsc  22147  kqcldsat  22348  elmptrab  22442  itg2uba  24357  prmorcht  25773  adjeq  29728  lnopcnbd  29829  cvexchlem  30161  maprnin  30503  topfne  33830  ismblfin  35117  ftc1anclem5  35153  isdmn2  35512  cdlemefrs29pre00  37710  cdlemefrs29cpre1  37713  isdomn3  40191  elmapintab  40339  bits0ALTV  44240
 Copyright terms: Public domain W3C validator