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

Theorem baib 904
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 299 . 2 (𝜓 → (𝜒 ↔ (𝜓𝜒)))
2 baib.1 . 2 (𝜑 ↔ (𝜓𝜒))
31, 2syl6rbbr 198 1 (𝜓 → (𝜑𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  baibr  905  rbaib  906  ceqsrexbv  2816  elrab3  2841  rabsn  3590  elrint2  3812  frind  4274  fnres  5239  f1ompt  5571  fliftfun  5697  ovid  5887  brdifun  6456  xpcomco  6720  ltexprlemdisj  7426  xrlenlt  7841  reapval  8350  znnnlt1  9114  difrp  9492  elfz  9808  fzolb2  9943  elfzo3  9952  fzouzsplit  9968  rpexp  11842  bastop1  12266  cnntr  12408  lmres  12431  tx1cn  12452  tx2cn  12453  xmetec  12620
  Copyright terms: Public domain W3C validator