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  1192  3biant1d  1392  drex1  1847  elrab3t  2974  eldifvsn  3828  bnd2  4288  opbrop  4831  opelresi  5051  funcnv3  5420  fnssresb  5472  dff1o5  5625  fneqeql2  5789  fnniniseg2  5803  dffo3  5826  fmptco  5845  fnressn  5872  fconst4m  5906  riota2df  6027  eloprabga  6142  suppimacnvfn  6448  mptsuppd  6458  suppssrst  6463  suppssrgst  6464  frecabcl  6632  mptelixpg  6971  exmidfodomrlemreseldju  7505  enq0breq  7753  genpassl  7841  genpassu  7842  elnnnn0  9541  peano2z  9615  znnsub  9631  znn0sub  9645  uzin  9890  nn01to3  9952  rpnegap  10022  negelrp  10023  xsubge0  10217  divelunit  10338  elfz5  10354  uzsplit  10430  elfzonelfzo  10579  infssuzex  10597  adddivflid  10656  divfl0  10660  hashfibclem  11210  swrdspsleq  11363  2shfti  11520  rexuz3  11679  clim2c  11973  fisumss  12082  bitsmod  12646  bitscmp  12648  bezoutlemmain  12698  nninfctlemfo  12740  dvdsfi  12940  pc2dvds  13032  1arith  13069  xpsfrnel  13574  xpsfrnel2  13576  ghmeqker  14005  lsslss  14546  zndvds  14814  znleval2  14819  eltg3  14939  lmbrf  15097  cnrest2  15118  cnptoprest  15121  cnptoprest2  15122  ismet2  15236  elbl2ps  15274  elbl2  15275  xblpnfps  15280  xblpnf  15281  bdxmet  15383  metcn  15396  cnbl0  15416  cnblcld  15417  mulc1cncf  15471  ellimc3apf  15542  pilem1  15661  wilthlem1  15865  lgsdilem  15917  lgsne0  15928  lgsabs1  15929  lgsquadlem1  15967  lgsquadlem2  15968  isclwwlknx  16428  clwwlkn1  16430