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

Theorem rbaib 534
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 533 . 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  1721  reusv1  5099  reusv2lem1  5100  opelresgOLD2  5643  fpwwe2  9787  fzsplit2  12666  saddisjlem  15566  smupval  15590  smueqlem  15592  prmrec  16004  ablnsg  18610  cnprest  21471  flimrest  22164  fclsrest  22205  tsmssubm  22323  setsxms  22661  tcphcph  23412  ellimc2  24047  fsumvma2  25359  chpub  25365  mdbr2  29706  mdsl2i  29732  fzsplit3  30096  posrasymb  30198  trleile  30207  cnvcnvintabd  38742
  Copyright terms: Public domain W3C validator