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

Theorem baib 837
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 289 . 2 (𝜓 → (𝜒 ↔ (𝜓𝜒)))
2 baib.1 . 2 (𝜑 ↔ (𝜓𝜒))
31, 2syl6rbbr 192 1 (𝜓 → (𝜑𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 101  wb 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  baibr  838  rbaib  839  ceqsrexbv  2695  elrab3  2719  dfpss3  3055  rabsn  3462  elrint2  3681  frind  4114  fnres  5040  f1ompt  5345  fliftfun  5461  ovid  5642  brdifun  6161  xpcomco  6328  ltexprlemdisj  6732  xrlenlt  7113  reapval  7611  znnnlt1  8320  difrp  8687  elfz  8952  fzolb2  9082  elfzo3  9091  fzouzsplit  9107
  Copyright terms: Public domain W3C validator