Theorem biantrurd 305

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

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

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  mpbirand  441  3anibar  1165  drex1  1798  elrab3t  2892  bnd2  4173  opbrop  4705  opelresi  4918  funcnv3  5278  fnssresb  5328  dff1o5  5470  fneqeql2  5625  fnniniseg2  5639  rexsupp  5640  dffo3  5663  fmptco  5682  fnressn  5702  fconst4m  5736  riota2df  5850  eloprabga  5961  frecabcl  6399  mptelixpg  6733  exmidfodomrlemreseldju  7198  enq0breq  7434  genpassl  7522  genpassu  7523  elnnnn0  9218  peano2z  9288  znnsub  9303  znn0sub  9317  uzin  9559  nn01to3  9616  rpnegap  9685  negelrp  9686  xsubge0  9880  divelunit  10001  elfz5  10016  uzsplit  10091  elfzonelfzo  10229  adddivflid  10291  divfl0  10295  2shfti  10839  rexuz3  10998  clim2c  11291  fisumss  11399  infssuzex  11949  bezoutlemmain  11998  pc2dvds  12328  1arith  12364  xpsfrnel  12762  xpsfrnel2  12764  eltg3  13527  lmbrf  13685  cnrest2  13706  cnptoprest  13709  cnptoprest2  13710  ismet2  13824  elbl2ps  13862  elbl2  13863  xblpnfps  13868  xblpnf  13869  bdxmet  13971  metcn  13984  cnbl0  14004  cnblcld  14005  mulc1cncf  14046  ellimc3apf  14099  pilem1  14170  lgsdilem  14398  lgsne0  14409  lgsabs1  14410