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

Theorem baibr 944
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 943 . 2 (𝜓 → (𝜑𝜒))
32bicomd 213 1 (𝜓 → (𝜒𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384
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 197  df-an 386
This theorem is referenced by:  pm5.44  949  exmoeu2  2495  ssnelpss  3710  brinxp  5171  copsex2ga  5221  canth  6593  riotaxfrd  6627  iscard  8786  kmlem14  8970  ltxrlt  10093  elioo5  12216  prmind2  15379  pcelnn  15555  isnirred  18681  isreg2  21162  comppfsc  21316  kqcldsat  21517  elmptrab  21611  itg2uba  23491  prmorcht  24885  adjeq  28764  lnopcnbd  28865  cvexchlem  29197  maprnin  29480  topfne  32324  ismblfin  33421  ftc1anclem5  33460  isdmn2  33825  cdlemefrs29pre00  35502  cdlemefrs29cpre1  35505  isdomn3  37601  elmapintab  37721  bits0ALTV  41355
  Copyright terms: Public domain W3C validator