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

Theorem ibar 299
 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 138 . 2 (𝜑 → (𝜓 → (𝜑𝜓)))
2 simpr 109 . 2 ((𝜑𝜓) → 𝜓)
31, 2impbid1 141 1 (𝜑 → (𝜓 ↔ (𝜑𝜓)))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 106  ax-ia3 107 This theorem depends on definitions:  df-bi 116 This theorem is referenced by:  biantrur  301  biantrurd  303  anclb  317  pm5.42  318  pm5.32  448  anabs5  562  pm5.33  598  bianabs  600  baib  904  baibd  908  anxordi  1378  euan  2055  eueq3dc  2858  ifandc  3508  xpcom  5085  fvopab3g  5494  riota1a  5749  ctssdccl  6996  recmulnqg  7206  ltexprlemloc  7422  mul0eqap  8438  eluz2  9339  rpnegap  9481  elfz2  9804  zmodid2  10132  shftfib  10602  dvdsssfz1  11556  modremain  11632  ctiunctlemudc  11956  txcnmpt  12451  reopnap  12716  ellimc3apf  12807
 Copyright terms: Public domain W3C validator