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  2625  ssnelpss  4013  brinxp  5521  copsex2ga  5571  canth  6979  riotaxfrd  7013  iscard  9255  kmlem14  9440  ltxrlt  10563  elioo5  12649  prmind2  15863  pcelnn  16040  isnirred  19145  isreg2  21674  comppfsc  21829  kqcldsat  22030  elmptrab  22124  itg2uba  24032  prmorcht  25442  adjeq  29408  lnopcnbd  29509  cvexchlem  29841  maprnin  30160  topfne  33317  ismblfin  34489  ftc1anclem5  34527  isdmn2  34890  cdlemefrs29pre00  37087  cdlemefrs29cpre1  37090  isdomn3  39314  elmapintab  39466  bits0ALTV  43352
  Copyright terms: Public domain W3C validator