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

Theorem rbaib 542
 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 541 . 2 (𝜒 → (𝜓𝜑))
32bicomd 226 1 (𝜒 → (𝜑𝜓))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399 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 210  df-an 400 This theorem is referenced by:  pm5.75  1026  cador  1610  reusv1  5266  reusv2lem1  5267  fpwwe2  10103  fzsplit2  12981  saddisjlem  15863  smupval  15887  smueqlem  15889  prmrec  16313  ablnsg  19035  cnprest  21989  flimrest  22683  fclsrest  22724  tsmssubm  22843  setsxms  23181  tcphcph  23937  ellimc2  24576  fsumvma2  25897  chpub  25903  mdbr2  30178  mdsl2i  30204  fzsplit3  30639  posrasymb  30766  trleile  30775  fvineqsneu  35108  cnvcnvintabd  40673  grumnud  41367
 Copyright terms: Public domain W3C validator