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

Theorem rbaib 945
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 944 . 2 (𝜒 → (𝜓𝜑))
32bicomd 212 1 (𝜒 → (𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195  wa 383
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 196  df-an 385
This theorem is referenced by:  cador  1538  reusv1  4792  reusv1OLD  4793  reusv2lem1  4794  opres  5326  cores  5555  fvres  6117  fpwwe2  9344  fzsplit2  12237  saddisjlem  15024  smupval  15048  smueqlem  15050  prmrec  15464  ablnsg  18073  cnprest  20903  flimrest  21597  fclsrest  21638  tsmssubm  21756  setsxms  22094  tchcph  22844  ellimc2  23447  fsumvma2  24739  chpub  24745  mdbr2  28539  mdsl2i  28565  fzsplit3  28940  posrasymb  28988  trleile  28997  cnvcnvintabd  36925
  Copyright terms: Public domain W3C validator