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  4351  fnres  5331  f1ompt  5666  fliftfun  5794  ovid  5988  brdifun  6559  xpcomco  6823  ltexprlemdisj  7602  xrlenlt  8018  reapval  8529  znnnlt1  9297  difrp  9688  elfz  10010  fzolb2  10149  elfzo3  10158  fzouzsplit  10174  rpexp  12145  isabl2  13028  bastop1  13454  cnntr  13596  lmres  13619  tx1cn  13640  tx2cn  13641  xmetec  13808  lgsabs1  14311
  Copyright terms: Public domain W3C validator