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

Theorem ibar 289
Description: Introduction of antecedent as conjunct. (Contributed by NM, 5-Dec-1995.) (Revised by NM, 24-Mar-2013.)
Assertion
Ref Expression
ibar (𝜑 → (𝜓 ↔ (𝜑𝜓)))

Proof of Theorem ibar
StepHypRef Expression
1 pm3.2 130 . 2 (𝜑 → (𝜓 → (𝜑𝜓)))
2 simpr 107 . 2 ((𝜑𝜓) → 𝜓)
31, 2impbid1 134 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-ia2 104  ax-ia3 105
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  biantrur  291  biantrurd  293  anclb  306  pm5.42  307  pm5.32  434  anabs5  515  pm5.33  551  bianabs  553  baib  839  baibd  843  anxordi  1307  euan  1972  eueq3dc  2738  xpcom  4892  fvopab3g  5273  riota1a  5515  recmulnqg  6547  ltexprlemloc  6763  eluz2  8575  rpnegap  8713  elfz2  8983  zmodid2  9302  shftfib  9652  dvdsssfz1  10164  modremain  10241
  Copyright terms: Public domain W3C validator