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  562  pm5.33  598  bianabs  600  baib  904  baibd  908  anxordi  1378  euan  2053  eueq3dc  2853  ifandc  3503  xpcom  5080  fvopab3g  5487  riota1a  5742  ctssdccl  6989  recmulnqg  7192  ltexprlemloc  7408  mul0eqap  8424  eluz2  9325  rpnegap  9467  elfz2  9790  zmodid2  10118  shftfib  10588  dvdsssfz1  11539  modremain  11615  ctiunctlemudc  11939  txcnmpt  12431  reopnap  12696  ellimc3apf  12787
  Copyright terms: Public domain W3C validator