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  1167  drex1  1812  elrab3t  2919  bnd2  4207  opbrop  4743  opelresi  4958  funcnv3  5321  fnssresb  5373  dff1o5  5516  fneqeql2  5674  fnniniseg2  5688  rexsupp  5689  dffo3  5712  fmptco  5731  fnressn  5751  fconst4m  5785  riota2df  5901  eloprabga  6013  frecabcl  6466  mptelixpg  6802  exmidfodomrlemreseldju  7279  enq0breq  7520  genpassl  7608  genpassu  7609  elnnnn0  9309  peano2z  9379  znnsub  9394  znn0sub  9408  uzin  9651  nn01to3  9708  rpnegap  9778  negelrp  9779  xsubge0  9973  divelunit  10094  elfz5  10109  uzsplit  10184  elfzonelfzo  10323  infssuzex  10340  adddivflid  10399  divfl0  10403  2shfti  11013  rexuz3  11172  clim2c  11466  fisumss  11574  bitsmod  12138  bitscmp  12140  bezoutlemmain  12190  nninfctlemfo  12232  dvdsfi  12432  pc2dvds  12524  1arith  12561  xpsfrnel  13046  xpsfrnel2  13048  ghmeqker  13477  lsslss  14013  zndvds  14281  znleval2  14286  eltg3  14377  lmbrf  14535  cnrest2  14556  cnptoprest  14559  cnptoprest2  14560  ismet2  14674  elbl2ps  14712  elbl2  14713  xblpnfps  14718  xblpnf  14719  bdxmet  14821  metcn  14834  cnbl0  14854  cnblcld  14855  mulc1cncf  14909  ellimc3apf  14980  pilem1  15099  wilthlem1  15300  lgsdilem  15352  lgsne0  15363  lgsabs1  15364  lgsquadlem1  15402  lgsquadlem2  15403