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

Theorem rbaib 539
Description: Move conjunction outside of biconditional. (Contributed by Mario Carneiro, 11-Sep-2015.) (Proof shortened by Wolf Lammen, 19-Jan-2020.)
Hypothesis
Ref Expression
baib.1 (𝜑 ↔ (𝜓𝜒))
Assertion
Ref Expression
rbaib (𝜒 → (𝜑𝜓))

Proof of Theorem rbaib
StepHypRef Expression
1 baib.1 . . 3 (𝜑 ↔ (𝜓𝜒))
21rbaibr 538 . 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:  pm5.75  1024  cador  1602  reusv1  5294  reusv2lem1  5295  fpwwe2  10059  fzsplit2  12927  saddisjlem  15808  smupval  15832  smueqlem  15834  prmrec  16253  ablnsg  18903  cnprest  21832  flimrest  22526  fclsrest  22567  tsmssubm  22685  setsxms  23023  tcphcph  23774  ellimc2  24409  fsumvma2  25723  chpub  25729  mdbr2  30006  mdsl2i  30032  fzsplit3  30449  posrasymb  30577  trleile  30586  fvineqsneu  34580  cnvcnvintabd  39844  grumnud  40506
  Copyright terms: Public domain W3C validator