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

Theorem rbaib 898
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 450 . . 3  |-  ( ( ps  /\  ch )  <->  ( ch  /\  ps )
)
31, 2bitri 249 . 2  |-  ( ph  <->  ( ch  /\  ps )
)
43baib 896 1  |-  ( ch 
->  ( ph  <->  ps )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369
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 185  df-an 371
This theorem is referenced by:  cador  1432  reusv1  4492  reusv2lem1  4493  opres  5120  cores  5341  fvres  5704  fpwwe2  8810  fzsplit2  11474  saddisjlem  13660  smupval  13684  smueqlem  13686  prmrec  13983  ablnsg  16329  cnprest  18893  flimrest  19556  fclsrest  19597  tsmssubm  19716  setsxms  20054  tchcph  20752  ellimc2  21352  fsumvma2  22553  chpub  22559  mdbr2  25700  mdsl2i  25726  fzsplit3  26078  posrasymb  26118  trleile  26127
  Copyright terms: Public domain W3C validator