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

Theorem rbaib 914
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  |-  ( ph  <->  ( ps  /\  ch )
)
Assertion
Ref Expression
rbaib  |-  ( ch 
->  ( ph  <->  ps )
)

Proof of Theorem rbaib
StepHypRef Expression
1 baib.1 . . 3  |-  ( ph  <->  ( ps  /\  ch )
)
21rbaibr 913 . 2  |-  ( ch 
->  ( ps  <->  ph ) )
32bicomd 204 1  |-  ( ch 
->  ( ph  <->  ps )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    /\ wa 370
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 188  df-an 372
This theorem is referenced by:  cador  1506  reusv1  4625  reusv2lem1  4626  opres  5134  cores  5358  fvres  5895  fpwwe2  9067  fzsplit2  11822  saddisjlem  14412  smupval  14436  smueqlem  14438  prmrec  14829  ablnsg  17420  cnprest  20236  flimrest  20929  fclsrest  20970  tsmssubm  21088  setsxms  21425  tchcph  22104  ellimc2  22709  fsumvma2  24005  chpub  24011  mdbr2  27784  mdsl2i  27810  fzsplit3  28206  posrasymb  28256  trleile  28265
  Copyright terms: Public domain W3C validator