MPE Home 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  2579  ssnelpss  4026  brinxp  5627  copsex2ga  5677  canth  7167  riotaxfrd  7205  iscard  9591  kmlem14  9777  ltxrlt  10903  elioo5  12992  prmind2  16242  pcelnn  16423  isnirred  19718  isreg2  22274  comppfsc  22429  kqcldsat  22630  elmptrab  22724  itg2uba  24641  prmorcht  26060  adjeq  30016  lnopcnbd  30117  cvexchlem  30449  maprnin  30786  topfne  34280  ismblfin  35555  ftc1anclem5  35591  isdmn2  35950  cdlemefrs29pre00  38146  cdlemefrs29cpre1  38149  isdomn3  40732  elmapintab  40880  bits0ALTV  44804
  Copyright terms: Public domain W3C validator