Theorem biantrurd 305

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

Step	Hyp	Ref	Expression
1		biantrud.1	. 2 |- ( ph -> ps )
2		ibar 301	. 2 |- ( ps -> ( ch <-> ( ps /\ ch ) ) )
3	1, 2	syl 14	1 |- ( ph -> ( ch <-> ( ps /\ ch ) ) )

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:  mpbirand  445  3anibar  1196  3biant1d  1396  drex1  1851  elrab3t  2981  eldifvsn  3842  bnd2  4305  opbrop  4849  opelresi  5069  funcnv3  5438  fnssresb  5490  dff1o5  5643  fneqeql2  5809  fnniniseg2  5823  dffo3  5846  fmptco  5865  fnressn  5892  fconst4m  5926  riota2df  6050  eloprabga  6165  suppimacnvfn  6476  mptsuppd  6486  suppssrst  6491  suppssrgst  6492  frecabcl  6660  mptelixpg  7006  exmidfodomrlemreseldju  7542  enq0breq  7793  genpassl  7881  genpassu  7882  elnnnn0  9585  peano2z  9659  znnsub  9675  znn0sub  9689  uzin  9934  nn01to3  9996  rpnegap  10066  negelrp  10067  xsubge0  10262  divelunit  10383  elfz5  10399  uzsplit  10477  elfzonelfzo  10626  infssuzex  10644  adddivflid  10705  divfl0  10709  hashfibclem  11260  hashf1lem1  11263  swrdspsleq  11417  2shfti  11574  rexuz3  11734  clim2c  12028  fisumss  12137  bitsmod  12701  bitscmp  12703  bezoutlemmain  12753  nninfctlemfo  12795  dvdsfi  12995  pc2dvds  13087  1arith  13124  xpsfrnel  13642  xpsfrnel2  13644  ghmeqker  14051  lsslss  14690  zndvds  14956  znleval2  14961  eltg3  15081  lmbrf  15239  cnrest2  15260  cnptoprest  15263  cnptoprest2  15264  ismet2  15378  elbl2ps  15416  elbl2  15417  xblpnfps  15422  xblpnf  15423  bdxmet  15525  metcn  15538  cnbl0  15558  cnblcld  15559  mulc1cncf  15613  ellimc3apf  15684  pilem1  15803  wilthlem1  16008  lgsdilem  16060  lgsne0  16071  lgsabs1  16072  lgsquadlem1  16110  lgsquadlem2  16111  isclwwlknx  16571  clwwlkn1  16573