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

Theorem ibar 295
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 137 . 2  |-  ( ph  ->  ( ps  ->  ( ph  /\  ps ) ) )
2 simpr 108 . 2  |-  ( (
ph  /\  ps )  ->  ps )
31, 2impbid1 140 1  |-  ( ph  ->  ( ps  <->  ( ph  /\ 
ps ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102    <-> wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  biantrur  297  biantrurd  299  anclb  312  pm5.42  313  pm5.32  441  anabs5  540  pm5.33  576  bianabs  578  baib  866  baibd  870  anxordi  1336  euan  2004  eueq3dc  2789  ifandc  3427  xpcom  4977  fvopab3g  5377  riota1a  5627  recmulnqg  6948  ltexprlemloc  7164  eluz2  9023  rpnegap  9164  elfz2  9429  zmodid2  9755  shftfib  10253  dvdsssfz1  11127  modremain  11203
  Copyright terms: Public domain W3C validator