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

Theorem biantrurd 301
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 297 . 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  435  3anibar  1132  drex1  1752  elrab3t  2810  bnd2  4065  opbrop  4586  opelresi  4798  funcnv3  5153  fnssresb  5203  dff1o5  5342  fneqeql2  5495  fnniniseg2  5509  rexsupp  5510  dffo3  5533  fmptco  5552  fnressn  5572  fconst4m  5606  riota2df  5716  eloprabga  5824  frecabcl  6262  mptelixpg  6594  exmidfodomrlemreseldju  7020  enq0breq  7208  genpassl  7296  genpassu  7297  elnnnn0  8971  peano2z  9041  znnsub  9056  znn0sub  9070  uzin  9307  nn01to3  9358  rpnegap  9422  xsubge0  9604  divelunit  9725  elfz5  9738  uzsplit  9812  elfzonelfzo  9947  adddivflid  10005  divfl0  10009  2shfti  10543  rexuz3  10702  clim2c  10993  fisumss  11101  infssuzex  11538  bezoutlemmain  11582  eltg3  12121  lmbrf  12279  cnrest2  12300  cnptoprest  12303  cnptoprest2  12304  ismet2  12418  elbl2ps  12456  elbl2  12457  xblpnfps  12462  xblpnf  12463  bdxmet  12565  metcn  12578  cnbl0  12598  cnblcld  12599  mulc1cncf  12640  ellimc3apf  12681  pilem1  12743
  Copyright terms: Public domain W3C validator