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

Theorem baib 862
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  863  rbaib  864  ceqsrexbv  2727  elrab3  2751  rabsn  3467  elrint2  3685  frind  4115  fnres  5046  f1ompt  5352  fliftfun  5467  ovid  5648  brdifun  6199  xpcomco  6370  ltexprlemdisj  6858  xrlenlt  7244  reapval  7743  znnnlt1  8480  difrp  8851  elfz  9111  fzolb2  9240  elfzo3  9249  fzouzsplit  9265  rpexp  10676
  Copyright terms: Public domain W3C validator