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  538  pm5.33  574  bianabs  576  baib  862  baibd  866  anxordi  1332  euan  1998  eueq3dc  2767  xpcom  4894  fvopab3g  5277  riota1a  5518  recmulnqg  6643  ltexprlemloc  6859  eluz2  8706  rpnegap  8847  elfz2  9112  zmodid2  9434  shftfib  9849  dvdsssfz1  10397  modremain  10473
  Copyright terms: Public domain W3C validator