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

Theorem rbaib 528
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 527 . 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:  cador  1695  reusv1  4997  reusv2lem1  4998  opelresg  5540  opres  5547  cores  5782  fvres  6348  fpwwe2  9667  fzsplit2  12573  saddisjlem  15394  smupval  15418  smueqlem  15420  prmrec  15833  ablnsg  18457  cnprest  21314  flimrest  22007  fclsrest  22048  tsmssubm  22166  setsxms  22504  tchcph  23255  ellimc2  23861  fsumvma2  25160  chpub  25166  mdbr2  29495  mdsl2i  29521  fzsplit3  29893  posrasymb  29997  trleile  30006  cnvcnvintabd  38432
  Copyright terms: Public domain W3C validator