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

Theorem baib 866
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 295 . 2 (𝜓 → (𝜒 ↔ (𝜓𝜒)))
2 baib.1 . 2 (𝜑 ↔ (𝜓𝜒))
31, 2syl6rbbr 197 1 (𝜓 → (𝜑𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  baibr  867  rbaib  868  ceqsrexbv  2746  elrab3  2770  rabsn  3504  elrint2  3724  frind  4170  fnres  5116  f1ompt  5434  fliftfun  5557  ovid  5743  brdifun  6299  xpcomco  6522  ltexprlemdisj  7144  xrlenlt  7530  reapval  8029  znnnlt1  8768  difrp  9139  elfz  9399  fzolb2  9530  elfzo3  9539  fzouzsplit  9555  rpexp  11225
  Copyright terms: Public domain W3C validator