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

Theorem baib 885
 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 297 . 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-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107 This theorem depends on definitions:  df-bi 116 This theorem is referenced by:  baibr  886  rbaib  887  ceqsrexbv  2784  elrab3  2808  rabsn  3554  elrint2  3776  frind  4232  fnres  5195  f1ompt  5523  fliftfun  5649  ovid  5839  brdifun  6408  xpcomco  6671  ltexprlemdisj  7356  xrlenlt  7747  reapval  8250  znnnlt1  9000  difrp  9373  elfz  9683  fzolb2  9818  elfzo3  9827  fzouzsplit  9843  rpexp  11671  bastop1  12089  cnntr  12230  lmres  12253  tx1cn  12274  tx2cn  12275  xmetec  12420
 Copyright terms: Public domain W3C validator