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

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

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  438  3anibar  1150  drex1  1778  elrab3t  2867  bnd2  4137  opbrop  4668  opelresi  4880  funcnv3  5235  fnssresb  5285  dff1o5  5426  fneqeql2  5579  fnniniseg2  5593  rexsupp  5594  dffo3  5617  fmptco  5636  fnressn  5656  fconst4m  5690  riota2df  5803  eloprabga  5911  frecabcl  6349  mptelixpg  6682  exmidfodomrlemreseldju  7138  enq0breq  7359  genpassl  7447  genpassu  7448  elnnnn0  9139  peano2z  9209  znnsub  9224  znn0sub  9238  uzin  9477  nn01to3  9533  rpnegap  9600  negelrp  9601  xsubge0  9792  divelunit  9913  elfz5  9927  uzsplit  10001  elfzonelfzo  10139  adddivflid  10201  divfl0  10205  2shfti  10743  rexuz3  10902  clim2c  11193  fisumss  11301  infssuzex  11849  bezoutlemmain  11898  eltg3  12553  lmbrf  12711  cnrest2  12732  cnptoprest  12735  cnptoprest2  12736  ismet2  12850  elbl2ps  12888  elbl2  12889  xblpnfps  12894  xblpnf  12895  bdxmet  12997  metcn  13010  cnbl0  13030  cnblcld  13031  mulc1cncf  13072  ellimc3apf  13125  pilem1  13196