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

Theorem rbaib 944
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 943 . 2 (𝜒 → (𝜓𝜑))
32bicomd 211 1 (𝜒 → (𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  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 195  df-an 384
This theorem is referenced by:  cador  1537  reusv1  4784  reusv1OLD  4785  reusv2lem1  4786  opres  5310  cores  5538  fvres  6099  fpwwe2  9318  fzsplit2  12189  saddisjlem  14967  smupval  14991  smueqlem  14993  prmrec  15407  ablnsg  18016  cnprest  20842  flimrest  21536  fclsrest  21577  tsmssubm  21695  setsxms  22032  tchcph  22762  ellimc2  23361  fsumvma2  24653  chpub  24659  mdbr2  28342  mdsl2i  28368  fzsplit3  28743  posrasymb  28791  trleile  28800  cnvcnvintabd  36725
  Copyright terms: Public domain W3C validator