MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rbaib Structured version   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  1400  reusv1  4715  reusv2lem1  4716  opres  5147  cores  5365  fvres  5737  fpwwe2  8510  fzsplit2  11068  saddisjlem  12968  smupval  12992  smueqlem  12994  prmrec  13282  ablnsg  15454  cnprest  17345  flimrest  18007  fclsrest  18048  tsmssubm  18164  setsxms  18501  tchcph  19186  ellimc2  19756  fsumvma2  20990  chpub  20996  mdbr2  23791  mdsl2i  23817  fzsplit3  24142
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