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

Theorem rbaib 874
Description: Move conjunction outside of biconditional. (Contributed by Mario Carneiro, 11-Sep-2015.)
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 )
)
2 ancom 438 . . 3  |-  ( ( ps  /\  ch )  <->  ( ch  /\  ps )
)
31, 2bitri 241 . 2  |-  ( ph  <->  ( ch  /\  ps )
)
43baib 872 1  |-  ( ch 
->  ( ph  <->  ps )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359
This theorem is referenced by:  cador  1397  reusv1  4663  reusv2lem1  4664  opres  5095  cores  5313  fvres  5685  fpwwe2  8451  fzsplit2  11008  saddisjlem  12903  smupval  12927  smueqlem  12929  prmrec  13217  ablnsg  15389  cnprest  17275  flimrest  17936  fclsrest  17977  tsmssubm  18093  setsxms  18399  tchcph  19065  ellimc2  19631  fsumvma2  20865  chpub  20871  mdbr2  23647  mdsl2i  23673  fzsplit3  23986
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator