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  1072  drex1  1679  elrab3t  2697  bnd2  3926  opbrop  4419  opelresi  4623  funcnv3  4961  fnssresb  5011  dff1o5  5135  fneqeql2  5276  fnniniseg2  5290  rexsupp  5291  dffo3  5314  fmptco  5330  fnressn  5349  fconst4m  5381  riota2df  5488  eloprabga  5591  enq0breq  6534  genpassl  6622  genpassu  6623  elnnnn0  8225  peano2z  8281  znnsub  8296  znn0sub  8309  uzin  8505  nn01to3  8552  rpnegap  8615  divelunit  8870  elfz5  8882  uzsplit  8954  elfzonelfzo  9086  adddivflid  9134  divfl0  9138  2shfti  9432  rexuz3  9588  clim2c  9805