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

Theorem baib 919
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 baib.1 . 2  |-  ( ph  <->  ( ps  /\  ch )
)
2 ibar 301 . 2  |-  ( ps 
->  ( ch  <->  ( ps  /\ 
ch ) ) )
31, 2bitr4id 199 1  |-  ( ps 
->  ( ph  <->  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104    <-> wb 105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  baibr  920  rbaib  921  ceqsrexbv  2868  elrab3  2894  rabsn  3659  elrint2  3885  frind  4352  fnres  5332  f1ompt  5667  fliftfun  5796  ovid  5990  brdifun  6561  xpcomco  6825  ltexprlemdisj  7604  xrlenlt  8021  reapval  8532  znnnlt1  9300  difrp  9691  elfz  10013  fzolb2  10153  elfzo3  10162  fzouzsplit  10178  rpexp  12152  isabl2  13095  bastop1  13553  cnntr  13695  lmres  13718  tx1cn  13739  tx2cn  13740  xmetec  13907  lgsabs1  14410
  Copyright terms: Public domain W3C validator