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

Theorem baib 827
Description: Move conjunction outside of biconditional. (Contributed by NM, 13-May-1999.)
Hypothesis
Ref Expression
baib.1
Assertion
Ref Expression
baib

Proof of Theorem baib
StepHypRef Expression
1 ibar 285 . 2
2 baib.1 . 2
31, 2syl6rbbr 188 1
Colors of variables: wff set class
Syntax hints:   wi 4   wa 97   wb 98
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  baibr  828  rbaib  829  ceqsrexbv  2669  elrab3  2693  dfpss3  3024  rabsn  3428  elrint2  3647  fnres  4958  f1ompt  5263  fliftfun  5379  ovid  5559  brdifun  6069  xpcomco  6236  ltexprlemdisj  6580  xrlenlt  6881  reapval  7360  znnnlt1  8069  difrp  8394  elfz  8650  fzolb2  8780  elfzo3  8789  fzouzsplit  8805
  Copyright terms: Public domain W3C validator