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