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

Theorem baibr 538
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 537 . 2 (𝜓 → (𝜑𝜒))
32bicomd 222 1 (𝜓 → (𝜒𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397
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 206  df-an 398
This theorem is referenced by:  rbaibr  539  pm5.44  544  exmoeub  2575  ssnelpss  4112  brinxp  5755  copsex2ga  5808  canth  7362  riotaxfrd  7400  iscard  9970  kmlem14  10158  ltxrlt  11284  elioo5  13381  prmind2  16622  pcelnn  16803  isnirred  20234  isreg2  22881  comppfsc  23036  kqcldsat  23237  elmptrab  23331  itg2uba  25261  prmorcht  26682  adjeq  31188  lnopcnbd  31289  cvexchlem  31621  maprnin  31956  topfne  35239  ismblfin  36529  ftc1anclem5  36565  isdmn2  36923  cdlemefrs29pre00  39266  cdlemefrs29cpre1  39269  isdomn3  41946  elmapintab  42347  bits0ALTV  46347
  Copyright terms: Public domain W3C validator