ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ibar Unicode 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  |-  ( ph  ->  ( ps  <->  ( ph  /\ 
ps ) ) )

Proof of Theorem ibar
StepHypRef Expression
1 pm3.2 138 . 2  |-  ( ph  ->  ( ps  ->  ( ph  /\  ps ) ) )
2 simpr 109 . 2  |-  ( (
ph  /\  ps )  ->  ps )
31, 2impbid1 141 1  |-  ( ph  ->  ( ps  <->  ( ph  /\ 
ps ) ) )
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  547  pm5.33  583  bianabs  585  baib  889  baibd  893  anxordi  1363  euan  2033  eueq3dc  2831  ifandc  3478  xpcom  5055  fvopab3g  5462  riota1a  5717  ctssdccl  6964  recmulnqg  7167  ltexprlemloc  7383  mul0eqap  8399  eluz2  9300  rpnegap  9442  elfz2  9765  zmodid2  10093  shftfib  10563  dvdsssfz1  11477  modremain  11553  ctiunctlemudc  11877  txcnmpt  12369  reopnap  12634  ellimc3apf  12725
  Copyright terms: Public domain W3C validator