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

Theorem rbaib 946
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 945 . 2 (𝜒 → (𝜓𝜑))
32bicomd 213 1 (𝜒 → (𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384
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 386
This theorem is referenced by:  cador  1544  reusv1  4836  reusv1OLD  4837  reusv2lem1  4838  opres  5375  cores  5607  fvres  6174  fpwwe2  9425  fzsplit2  12324  saddisjlem  15129  smupval  15153  smueqlem  15155  prmrec  15569  ablnsg  18190  cnprest  21033  flimrest  21727  fclsrest  21768  tsmssubm  21886  setsxms  22224  tchcph  22976  ellimc2  23581  fsumvma2  24873  chpub  24879  mdbr2  29043  mdsl2i  29069  fzsplit3  29436  posrasymb  29484  trleile  29493  cnvcnvintabd  37426
  Copyright terms: Public domain W3C validator