Theorem biantrurd 303

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

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  mpbirand  439  3anibar  1160  drex1  1791  elrab3t  2885  bnd2  4159  opbrop  4690  opelresi  4902  funcnv3  5260  fnssresb  5310  dff1o5  5451  fneqeql2  5605  fnniniseg2  5619  rexsupp  5620  dffo3  5643  fmptco  5662  fnressn  5682  fconst4m  5716  riota2df  5829  eloprabga  5940  frecabcl  6378  mptelixpg  6712  exmidfodomrlemreseldju  7177  enq0breq  7398  genpassl  7486  genpassu  7487  elnnnn0  9178  peano2z  9248  znnsub  9263  znn0sub  9277  uzin  9519  nn01to3  9576  rpnegap  9643  negelrp  9644  xsubge0  9838  divelunit  9959  elfz5  9973  uzsplit  10048  elfzonelfzo  10186  adddivflid  10248  divfl0  10252  2shfti  10795  rexuz3  10954  clim2c  11247  fisumss  11355  infssuzex  11904  bezoutlemmain  11953  pc2dvds  12283  1arith  12319  eltg3  12851  lmbrf  13009  cnrest2  13030  cnptoprest  13033  cnptoprest2  13034  ismet2  13148  elbl2ps  13186  elbl2  13187  xblpnfps  13192  xblpnf  13193  bdxmet  13295  metcn  13308  cnbl0  13328  cnblcld  13329  mulc1cncf  13370  ellimc3apf  13423  pilem1  13494  lgsdilem  13722  lgsne0  13733  lgsabs1  13734