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

Theorem ibar 285
 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 126 . 2 (𝜑 → (𝜓 → (𝜑𝜓)))
2 simpr 103 . 2 ((𝜑𝜓) → 𝜓)
31, 2impbid1 130 1 (𝜑 → (𝜓 ↔ (𝜑𝜓)))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia2 100  ax-ia3 101 This theorem depends on definitions:  df-bi 110 This theorem is referenced by:  biantrur  287  biantrurd  289  anclb  302  pm5.42  303  pm5.32  426  anabs5  507  pm5.33  541  bianabs  543  baib  828  baibd  832  anxordi  1291  euan  1956  eueq3dc  2715  xpcom  4864  fvopab3g  5245  riota1a  5487  recmulnqg  6489  ltexprlemloc  6705  eluz2  8479  rpnegap  8615  elfz2  8881  shftfib  9424
 Copyright terms: Public domain W3C validator