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  1189  3biant1d  1389  drex1  1844  elrab3t  2959  bnd2  4259  opbrop  4801  opelresi  5020  funcnv3  5387  fnssresb  5439  dff1o5  5587  fneqeql2  5750  fnniniseg2  5764  rexsupp  5765  dffo3  5788  fmptco  5807  fnressn  5833  fconst4m  5867  riota2df  5986  eloprabga  6101  frecabcl  6558  mptelixpg  6896  exmidfodomrlemreseldju  7399  enq0breq  7644  genpassl  7732  genpassu  7733  elnnnn0  9433  peano2z  9503  znnsub  9519  znn0sub  9533  uzin  9777  nn01to3  9839  rpnegap  9909  negelrp  9910  xsubge0  10104  divelunit  10225  elfz5  10240  uzsplit  10315  elfzonelfzo  10463  infssuzex  10481  adddivflid  10540  divfl0  10544  swrdspsleq  11235  2shfti  11379  rexuz3  11538  clim2c  11832  fisumss  11940  bitsmod  12504  bitscmp  12506  bezoutlemmain  12556  nninfctlemfo  12598  dvdsfi  12798  pc2dvds  12890  1arith  12927  xpsfrnel  13414  xpsfrnel2  13416  ghmeqker  13845  lsslss  14382  zndvds  14650  znleval2  14655  eltg3  14768  lmbrf  14926  cnrest2  14947  cnptoprest  14950  cnptoprest2  14951  ismet2  15065  elbl2ps  15103  elbl2  15104  xblpnfps  15109  xblpnf  15110  bdxmet  15212  metcn  15225  cnbl0  15245  cnblcld  15246  mulc1cncf  15300  ellimc3apf  15371  pilem1  15490  wilthlem1  15691  lgsdilem  15743  lgsne0  15754  lgsabs1  15755  lgsquadlem1  15793  lgsquadlem2  15794  isclwwlknx  16201  clwwlkn1  16203