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

Theorem biantrurd 303
Description: A wff is equivalent to its conjunction with truth. (Contributed by NM, 1-May-1995.) (Proof shortened by Andrew Salmon, 7-May-2011.)
Hypothesis
Ref Expression
biantrud.1  |-  ( ph  ->  ps )
Assertion
Ref Expression
biantrurd  |-  ( ph  ->  ( ch  <->  ( ps  /\ 
ch ) ) )

Proof of Theorem biantrurd
StepHypRef Expression
1 biantrud.1 . 2  |-  ( ph  ->  ps )
2 ibar 299 . 2  |-  ( ps 
->  ( ch  <->  ( ps  /\ 
ch ) ) )
31, 2syl 14 1  |-  ( ph  ->  ( ch  <->  ( ps  /\ 
ch ) ) )
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:  mpbirand  437  3anibar  1134  drex1  1754  elrab3t  2812  bnd2  4067  opbrop  4588  opelresi  4800  funcnv3  5155  fnssresb  5205  dff1o5  5344  fneqeql2  5497  fnniniseg2  5511  rexsupp  5512  dffo3  5535  fmptco  5554  fnressn  5574  fconst4m  5608  riota2df  5718  eloprabga  5826  frecabcl  6264  mptelixpg  6596  exmidfodomrlemreseldju  7024  enq0breq  7212  genpassl  7300  genpassu  7301  elnnnn0  8988  peano2z  9058  znnsub  9073  znn0sub  9087  uzin  9326  nn01to3  9377  rpnegap  9442  negelrp  9443  xsubge0  9632  divelunit  9753  elfz5  9766  uzsplit  9840  elfzonelfzo  9975  adddivflid  10033  divfl0  10037  2shfti  10571  rexuz3  10730  clim2c  11021  fisumss  11129  infssuzex  11569  bezoutlemmain  11613  eltg3  12153  lmbrf  12311  cnrest2  12332  cnptoprest  12335  cnptoprest2  12336  ismet2  12450  elbl2ps  12488  elbl2  12489  xblpnfps  12494  xblpnf  12495  bdxmet  12597  metcn  12610  cnbl0  12630  cnblcld  12631  mulc1cncf  12672  ellimc3apf  12725  pilem1  12787
  Copyright terms: Public domain W3C validator