ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ibar Structured version   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  827  baibd  831  anxordi  1288  euan  1953  eueq3dc  2709  xpcom  4807  fvopab3g  5188  riota1a  5430  recmulnqg  6375  ltexprlemloc  6581  eluz2  8255  rpnegap  8390  elfz2  8651
  Copyright terms: Public domain W3C validator