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

Proof of Theorem ibar
StepHypRef Expression
1 pm3.2 139 . 2  |-  ( ph  ->  ( ps  ->  ( ph  /\  ps ) ) )
2 simpr 110 . 2  |-  ( (
ph  /\  ps )  ->  ps )
31, 2impbid1 142 1  |-  ( ph  ->  ( ps  <->  ( ph  /\ 
ps ) ) )
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  920  baibd  924  anxordi  1411  euan  2094  eueq3dc  2926  ifandc  3587  xpcom  5193  fvopab3g  5610  riota1a  5871  ctssdccl  7140  2omotaplemap  7286  recmulnqg  7420  ltexprlemloc  7636  mul0eqap  8657  eluz2  9564  rpnegap  9716  elfz2  10045  zmodid2  10383  shftfib  10864  dvdsssfz1  11890  modremain  11966  phisum  12272  ctiunctlemudc  12488  issubg  13112  resgrpisgrp  13134  qusecsub  13268  issubrng  13546  issubrg  13568  txcnmpt  14230  reopnap  14495  ellimc3apf  14586
  Copyright terms: Public domain W3C validator