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

Theorem rbaib 873
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 437 . . 3  |-  ( ( ps  /\  ch )  <->  ( ch  /\  ps )
)
31, 2bitri 240 . 2  |-  ( ph  <->  ( ch  /\  ps )
)
43baib 871 1  |-  ( ch 
->  ( ph  <->  ps )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358
This theorem is referenced by:  cador  1381  reusv1  4550  reusv2lem1  4551  opres  4980  cores  5192  fvres  5558  fpwwe2  8281  fzsplit2  10831  saddisjlem  12671  smupval  12695  smueqlem  12697  prmrec  12985  ablnsg  15155  cnprest  17033  flimrest  17694  fclsrest  17735  tsmssubm  17841  setsxms  18041  tchcph  18683  ellimc2  19243  fsumvma2  20469  chpub  20475  mdbr2  22892  mdsl2i  22918  fzsplit3  23047
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 177  df-an 360
  Copyright terms: Public domain W3C validator