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 ) ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  mpbirand  445  3anibar  1196  3biant1d  1396  drex1  1851  elrab3t  2981  eldifvsn  3847  bnd2  4310  opbrop  4854  opelresi  5074  funcnv3  5443  fnssresb  5495  dff1o5  5648  fneqeql2  5818  fnniniseg2  5832  dffo3  5855  fmptco  5874  fnressn  5901  fconst4m  5935  riota2df  6060  eloprabga  6175  suppimacnvfn  6486  mptsuppd  6496  suppssrst  6501  suppssrgst  6502  frecabcl  6670  mptelixpg  7016  exmidfodomrlemreseldju  7553  enq0breq  7804  genpassl  7892  genpassu  7893  elnnnn0  9611  peano2z  9685  znnsub  9701  znn0sub  9715  uzin  9965  nn01to3  10027  rpnegap  10098  negelrp  10099  xsubge0  10294  divelunit  10415  elfz5  10431  uzsplit  10510  elfzonelfzo  10659  infssuzex  10677  adddivflid  10742  divfl0  10746  hashfibclem  11298  hashf1lem1  11301  swrdspsleq  11455  2shfti  11612  rexuz3  11772  clim2c  12069  fisumss  12178  bitsmod  12742  bitscmp  12744  bezoutlemmain  12794  nninfctlemfo  12836  dvdsfi  13040  pc2dvds  13132  1arith  13169  xpsfrnel  13718  xpsfrnel2  13720  ghmeqker  14127  lsslss  14802  zndvds  15068  znleval2  15073  eltg3  15249  lmbrf  15407  cnrest2  15428  cnptoprest  15431  cnptoprest2  15432  ismet2  15546  elbl2ps  15584  elbl2  15585  xblpnfps  15590  xblpnf  15591  bdxmet  15693  metcn  15706  cnbl0  15726  cnblcld  15727  mulc1cncf  15781  ellimc3apf  15852  pilem1  15972  wilthlem1  16193  bposlem1  16272  lgsdilem  16312  lgsne0  16323  lgsabs1  16324  lgsquadlem1  16362  lgsquadlem2  16363  isclwwlknx  16823  clwwlkn1  16825