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  441  3anibar  1168  3biant1d  1367  drex1  1821  elrab3t  2928  bnd2  4218  opbrop  4755  opelresi  4971  funcnv3  5337  fnssresb  5389  dff1o5  5533  fneqeql2  5691  fnniniseg2  5705  rexsupp  5706  dffo3  5729  fmptco  5748  fnressn  5772  fconst4m  5806  riota2df  5922  eloprabga  6034  frecabcl  6487  mptelixpg  6823  exmidfodomrlemreseldju  7310  enq0breq  7551  genpassl  7639  genpassu  7640  elnnnn0  9340  peano2z  9410  znnsub  9426  znn0sub  9440  uzin  9683  nn01to3  9740  rpnegap  9810  negelrp  9811  xsubge0  10005  divelunit  10126  elfz5  10141  uzsplit  10216  elfzonelfzo  10361  infssuzex  10378  adddivflid  10437  divfl0  10441  swrdspsleq  11123  2shfti  11175  rexuz3  11334  clim2c  11628  fisumss  11736  bitsmod  12300  bitscmp  12302  bezoutlemmain  12352  nninfctlemfo  12394  dvdsfi  12594  pc2dvds  12686  1arith  12723  xpsfrnel  13209  xpsfrnel2  13211  ghmeqker  13640  lsslss  14176  zndvds  14444  znleval2  14449  eltg3  14562  lmbrf  14720  cnrest2  14741  cnptoprest  14744  cnptoprest2  14745  ismet2  14859  elbl2ps  14897  elbl2  14898  xblpnfps  14903  xblpnf  14904  bdxmet  15006  metcn  15019  cnbl0  15039  cnblcld  15040  mulc1cncf  15094  ellimc3apf  15165  pilem1  15284  wilthlem1  15485  lgsdilem  15537  lgsne0  15548  lgsabs1  15549  lgsquadlem1  15587  lgsquadlem2  15588