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

Theorem baibr 526
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 525 . 2 (𝜓 → (𝜑𝜒))
32bicomd 213 1 (𝜓 → (𝜒𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 382
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 383
This theorem is referenced by:  pm5.44  532  exmoeu2  2645  ssnelpss  3868  brinxp  5321  copsex2ga  5370  canth  6751  riotaxfrd  6785  iscard  9001  kmlem14  9187  ltxrlt  10310  elioo5  12436  prmind2  15605  pcelnn  15781  isnirred  18908  isreg2  21402  comppfsc  21556  kqcldsat  21757  elmptrab  21851  itg2uba  23730  prmorcht  25125  adjeq  29134  lnopcnbd  29235  cvexchlem  29567  maprnin  29846  topfne  32686  ismblfin  33783  ftc1anclem5  33821  isdmn2  34186  cdlemefrs29pre00  36204  cdlemefrs29cpre1  36207  isdomn3  38308  elmapintab  38428  bits0ALTV  42118
  Copyright terms: Public domain W3C validator