Theorem biantrurd 299

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

Syntax hints:   -> wi 4   /\ wa 102   <-> wb 103

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  3anibar  1107  drex1  1720  elrab3t  2749  bnd2  3955  opbrop  4445  opelresi  4651  funcnv3  4992  fnssresb  5042  dff1o5  5166  fneqeql2  5308  fnniniseg2  5322  rexsupp  5323  dffo3  5346  fmptco  5362  fnressn  5381  fconst4m  5413  riota2df  5519  eloprabga  5622  frecabcl  6048  enq0breq  6688  genpassl  6776  genpassu  6777  elnnnn0  8398  peano2z  8468  znnsub  8483  znn0sub  8497  uzin  8732  nn01to3  8783  rpnegap  8847  divelunit  9100  elfz5  9113  uzsplit  9185  elfzonelfzo  9316  adddivflid  9374  divfl0  9378  2shfti  9857  rexuz3  10014  clim2c  10261  infssuzex  10489  bezoutlemmain  10531