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  2870  elrab3  2896  rabsn  3661  elrint2  3887  frind  4354  fnres  5334  f1ompt  5669  fliftfun  5799  ovid  5993  brdifun  6564  xpcomco  6828  ltexprlemdisj  7607  xrlenlt  8024  reapval  8535  znnnlt1  9303  difrp  9694  elfz  10016  fzolb2  10156  elfzo3  10165  fzouzsplit  10181  rpexp  12155  isabl2  13102  bastop1  13622  cnntr  13764  lmres  13787  tx1cn  13808  tx2cn  13809  xmetec  13976  lgsabs1  14479
  Copyright terms: Public domain W3C validator