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

Theorem baib 866
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 295 . 2  |-  ( ps 
->  ( ch  <->  ( ps  /\ 
ch ) ) )
2 baib.1 . 2  |-  ( ph  <->  ( ps  /\  ch )
)
31, 2syl6rbbr 197 1  |-  ( ps 
->  ( ph  <->  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102    <-> wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  baibr  867  rbaib  868  ceqsrexbv  2748  elrab3  2772  rabsn  3509  elrint2  3729  frind  4179  fnres  5130  f1ompt  5450  fliftfun  5575  ovid  5761  brdifun  6319  xpcomco  6542  ltexprlemdisj  7165  xrlenlt  7551  reapval  8053  znnnlt1  8798  difrp  9170  elfz  9430  fzolb2  9565  elfzo3  9574  fzouzsplit  9590  rpexp  11410
  Copyright terms: Public domain W3C validator