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

Theorem baib 828
 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  829  rbaib  830  ceqsrexbv  2675  elrab3  2699  dfpss3  3030  rabsn  3437  elrint2  3656  frind  4089  fnres  5015  f1ompt  5320  fliftfun  5436  ovid  5617  brdifun  6133  xpcomco  6300  ltexprlemdisj  6704  xrlenlt  7084  reapval  7567  znnnlt1  8293  difrp  8619  elfz  8880  fzolb2  9010  elfzo3  9019  fzouzsplit  9035
 Copyright terms: Public domain W3C validator