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

Theorem rbaib 540
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 539 . 2 (𝜒 → (𝜓𝜑))
32bicomd 222 1 (𝜒 → (𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397
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 206  df-an 398
This theorem is referenced by:  pm5.75  1028  cador  1610  reusv1  5356  reusv2lem1  5357  fpwwe2  10587  fzsplit2  13475  saddisjlem  16352  smupval  16376  smueqlem  16378  prmrec  16802  ablnsg  19633  cnprest  22663  flimrest  23357  fclsrest  23398  tsmssubm  23517  setsxms  23857  tcphcph  24624  ellimc2  25264  fsumvma2  26585  chpub  26591  mdbr2  31287  mdsl2i  31313  fzsplit3  31751  posrasymb  31881  trleile  31887  fvineqsneu  35932  cnvcnvintabd  41964  grumnud  42658  mofeu  47004
  Copyright terms: Public domain W3C validator