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  437  3anibar  1149  drex1  1770  elrab3t  2839  bnd2  4097  opbrop  4618  opelresi  4830  funcnv3  5185  fnssresb  5235  dff1o5  5376  fneqeql2  5529  fnniniseg2  5543  rexsupp  5544  dffo3  5567  fmptco  5586  fnressn  5606  fconst4m  5640  riota2df  5750  eloprabga  5858  frecabcl  6296  mptelixpg  6628  exmidfodomrlemreseldju  7056  enq0breq  7244  genpassl  7332  genpassu  7333  elnnnn0  9020  peano2z  9090  znnsub  9105  znn0sub  9119  uzin  9358  nn01to3  9409  rpnegap  9474  negelrp  9475  xsubge0  9664  divelunit  9785  elfz5  9798  uzsplit  9872  elfzonelfzo  10007  adddivflid  10065  divfl0  10069  2shfti  10603  rexuz3  10762  clim2c  11053  fisumss  11161  infssuzex  11642  bezoutlemmain  11686  eltg3  12226  lmbrf  12384  cnrest2  12405  cnptoprest  12408  cnptoprest2  12409  ismet2  12523  elbl2ps  12561  elbl2  12562  xblpnfps  12567  xblpnf  12568  bdxmet  12670  metcn  12683  cnbl0  12703  cnblcld  12704  mulc1cncf  12745  ellimc3apf  12798  pilem1  12860