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  1155  drex1  1786  elrab3t  2881  bnd2  4152  opbrop  4683  opelresi  4895  funcnv3  5250  fnssresb  5300  dff1o5  5441  fneqeql2  5594  fnniniseg2  5608  rexsupp  5609  dffo3  5632  fmptco  5651  fnressn  5671  fconst4m  5705  riota2df  5818  eloprabga  5929  frecabcl  6367  mptelixpg  6700  exmidfodomrlemreseldju  7156  enq0breq  7377  genpassl  7465  genpassu  7466  elnnnn0  9157  peano2z  9227  znnsub  9242  znn0sub  9256  uzin  9498  nn01to3  9555  rpnegap  9622  negelrp  9623  xsubge0  9817  divelunit  9938  elfz5  9952  uzsplit  10027  elfzonelfzo  10165  adddivflid  10227  divfl0  10231  2shfti  10773  rexuz3  10932  clim2c  11225  fisumss  11333  infssuzex  11882  bezoutlemmain  11931  pc2dvds  12261  1arith  12297  eltg3  12697  lmbrf  12855  cnrest2  12876  cnptoprest  12879  cnptoprest2  12880  ismet2  12994  elbl2ps  13032  elbl2  13033  xblpnfps  13038  xblpnf  13039  bdxmet  13141  metcn  13154  cnbl0  13174  cnblcld  13175  mulc1cncf  13216  ellimc3apf  13269  pilem1  13340  lgsdilem  13568  lgsne0  13579  lgsabs1  13580