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

Theorem rbaib 537
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 536 . 2 (𝜒 → (𝜓𝜑))
32bicomd 222 1 (𝜒 → (𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394
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 395
This theorem is referenced by:  pm5.75  1026  cador  1601  reusv1  5400  reusv2lem1  5401  fpwwe2  10682  fzsplit2  13575  saddisjlem  16459  smupval  16483  smueqlem  16485  prmrec  16919  ablnsg  19840  cnprest  23276  flimrest  23970  fclsrest  24011  tsmssubm  24130  setsxms  24470  tcphcph  25248  ellimc2  25889  fsumvma2  27235  chpub  27241  mdbr2  32221  mdsl2i  32247  fzsplit3  32685  posrasymb  32823  trleile  32829  fvineqsneu  37066  cnvcnvintabd  43204  grumnud  43897  mofeu  48152
  Copyright terms: Public domain W3C validator