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  4534  reusv2lem1  4535  opres  4964  cores  5176  fvres  5542  fpwwe2  8265  fzsplit2  10815  saddisjlem  12655  smupval  12679  smueqlem  12681  prmrec  12969  ablnsg  15139  cnprest  17017  flimrest  17678  fclsrest  17719  tsmssubm  17825  setsxms  18025  tchcph  18667  ellimc2  19227  fsumvma2  20453  chpub  20459  mdbr2  22876  mdsl2i  22902  fzsplit3  23031
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