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  2958  bnd2  4257  opbrop  4798  opelresi  5016  funcnv3  5383  fnssresb  5435  dff1o5  5583  fneqeql2  5746  fnniniseg2  5760  rexsupp  5761  dffo3  5784  fmptco  5803  fnressn  5829  fconst4m  5863  riota2df  5982  eloprabga  6097  frecabcl  6551  mptelixpg  6889  exmidfodomrlemreseldju  7389  enq0breq  7634  genpassl  7722  genpassu  7723  elnnnn0  9423  peano2z  9493  znnsub  9509  znn0sub  9523  uzin  9767  nn01to3  9824  rpnegap  9894  negelrp  9895  xsubge0  10089  divelunit  10210  elfz5  10225  uzsplit  10300  elfzonelfzo  10448  infssuzex  10465  adddivflid  10524  divfl0  10528  swrdspsleq  11215  2shfti  11358  rexuz3  11517  clim2c  11811  fisumss  11919  bitsmod  12483  bitscmp  12485  bezoutlemmain  12535  nninfctlemfo  12577  dvdsfi  12777  pc2dvds  12869  1arith  12906  xpsfrnel  13393  xpsfrnel2  13395  ghmeqker  13824  lsslss  14361  zndvds  14629  znleval2  14634  eltg3  14747  lmbrf  14905  cnrest2  14926  cnptoprest  14929  cnptoprest2  14930  ismet2  15044  elbl2ps  15082  elbl2  15083  xblpnfps  15088  xblpnf  15089  bdxmet  15191  metcn  15204  cnbl0  15224  cnblcld  15225  mulc1cncf  15279  ellimc3apf  15350  pilem1  15469  wilthlem1  15670  lgsdilem  15722  lgsne0  15733  lgsabs1  15734  lgsquadlem1  15772  lgsquadlem2  15773  isclwwlknx  16158  clwwlkn1  16160