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

Theorem rbaib 538
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 537 . 2 (𝜒 → (𝜓𝜑))
32bicomd 223 1 (𝜒 → (𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395
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 207  df-an 396
This theorem is referenced by:  pm5.75  1031  cador  1608  reusv1  5397  reusv2lem1  5398  fpwwe2  10683  fzsplit2  13589  saddisjlem  16501  smupval  16525  smueqlem  16527  prmrec  16960  ablnsg  19865  cnprest  23297  flimrest  23991  fclsrest  24032  tsmssubm  24151  setsxms  24491  tcphcph  25271  ellimc2  25912  fsumvma2  27258  chpub  27264  mdbr2  32315  mdsl2i  32341  fzsplit3  32795  posrasymb  32955  trleile  32961  fvineqsneu  37412  cnvcnvintabd  43613  grumnud  44305  mofeu  48757
  Copyright terms: Public domain W3C validator