ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  baib Structured version   GIF 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  6579  xrlenlt  6861  reapval  7340  znnnlt1  8049  difrp  8374  elfz  8630  fzolb2  8760  elfzo3  8769  fzouzsplit  8785
  Copyright terms: Public domain W3C validator