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

Theorem rbaib 904
Description: Move conjunction outside of biconditional. (Contributed by Mario Carneiro, 11-Sep-2015.) (Proof shortened by Wolf Lammen, 19-Jan-2020.)
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 )
)
21rbaibr 903 . 2  |-  ( ch 
->  ( ps  <->  ph ) )
32bicomd 201 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  1442  reusv1  4647  reusv2lem1  4648  opres  5282  cores  5509  fvres  5879  fpwwe2  9020  fzsplit2  11709  saddisjlem  13972  smupval  13996  smueqlem  13998  prmrec  14298  ablnsg  16653  cnprest  19572  flimrest  20235  fclsrest  20276  tsmssubm  20395  setsxms  20733  tchcph  21431  ellimc2  22032  fsumvma2  23233  chpub  23239  mdbr2  26907  mdsl2i  26933  fzsplit3  27283  posrasymb  27323  trleile  27332
  Copyright terms: Public domain W3C validator