Theorem biantrurd 289

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 285	. 2 |- (ps -> (ch <-> (ps /\ ch)))
3	1, 2	syl 14	1 |- (ph -> (ch <-> (ps /\ ch)))

Syntax hints:   -> wi 4   /\ wa 97   <-> wb 98

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  3anibar  1071  drex1  1676  elrab3t  2691  bnd2  3917  opbrop  4362  opelresi  4566  funcnv3  4904  fnssresb  4954  dff1o5  5078  fneqeql2  5219  fnniniseg2  5233  rexsupp  5234  dffo3  5257  fmptco  5273  fnressn  5292  fconst4m  5324  riota2df  5431  eloprabga  5533  enq0breq  6419  genpassl  6507  genpassu  6508  elnnnn0  8001  peano2z  8057  znnsub  8072  znn0sub  8085  uzin  8281  nn01to3  8328  rpnegap  8390  divelunit  8640  elfz5  8652  uzsplit  8724  elfzonelfzo  8856