ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  baib Unicode version

Theorem baib 887
Description: Move conjunction outside of biconditional. (Contributed by NM, 13-May-1999.)
Hypothesis
Ref Expression
baib.1  |-  ( ph  <->  ( ps  /\  ch )
)
Assertion
Ref Expression
baib  |-  ( ps 
->  ( ph  <->  ch )
)

Proof of Theorem baib
StepHypRef Expression
1 ibar 297 . 2  |-  ( ps 
->  ( ch  <->  ( ps  /\ 
ch ) ) )
2 baib.1 . 2  |-  ( ph  <->  ( ps  /\  ch )
)
31, 2syl6rbbr 198 1  |-  ( ps 
->  ( ph  <->  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    <-> wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  baibr  888  rbaib  889  ceqsrexbv  2788  elrab3  2812  rabsn  3558  elrint2  3780  frind  4242  fnres  5207  f1ompt  5537  fliftfun  5663  ovid  5853  brdifun  6422  xpcomco  6686  ltexprlemdisj  7378  xrlenlt  7793  reapval  8301  znnnlt1  9056  difrp  9431  elfz  9747  fzolb2  9882  elfzo3  9891  fzouzsplit  9907  rpexp  11738  bastop1  12158  cnntr  12300  lmres  12323  tx1cn  12344  tx2cn  12345  xmetec  12512
  Copyright terms: Public domain W3C validator