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

Theorem rbaib 536
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 535 . 2 (𝜒 → (𝜓𝜑))
32bicomd 215 1 (𝜒 → (𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 386
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 199  df-an 387
This theorem is referenced by:  cador  1723  reusv1  5096  reusv2lem1  5097  opelresgOLD2  5638  fpwwe2  9779  fzsplit2  12658  saddisjlem  15558  smupval  15582  smueqlem  15584  prmrec  15996  ablnsg  18602  cnprest  21463  flimrest  22156  fclsrest  22197  tsmssubm  22315  setsxms  22653  tcphcph  23404  ellimc2  24039  fsumvma2  25351  chpub  25357  mdbr2  29709  mdsl2i  29735  fzsplit3  30099  posrasymb  30201  trleile  30210  cnvcnvintabd  38746
  Copyright terms: Public domain W3C validator