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

Theorem ibar 301
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 139 . 2 (𝜑 → (𝜓 → (𝜑𝜓)))
2 simpr 110 . 2 ((𝜑𝜓) → 𝜓)
31, 2impbid1 142 1 (𝜑 → (𝜓 ↔ (𝜑𝜓)))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  wb 105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 107  ax-ia3 108
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  biantrur  303  biantrurd  305  anclb  319  pm5.42  320  pm5.32  453  anabs5  573  pm5.33  609  bianabs  611  baib  919  baibd  923  anxordi  1400  euan  2082  eueq3dc  2912  ifandc  3573  xpcom  5176  fvopab3g  5590  riota1a  5850  ctssdccl  7110  2omotaplemap  7256  recmulnqg  7390  ltexprlemloc  7606  mul0eqap  8627  eluz2  9534  rpnegap  9686  elfz2  10015  zmodid2  10352  shftfib  10832  dvdsssfz1  11858  modremain  11934  phisum  12240  ctiunctlemudc  12438  issubg  13033  resgrpisgrp  13055  issubrg  13342  txcnmpt  13776  reopnap  14041  ellimc3apf  14132
  Copyright terms: Public domain W3C validator