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  1167  drex1  1809  elrab3t  2915  bnd2  4202  opbrop  4738  opelresi  4953  funcnv3  5316  fnssresb  5366  dff1o5  5509  fneqeql2  5667  fnniniseg2  5681  rexsupp  5682  dffo3  5705  fmptco  5724  fnressn  5744  fconst4m  5778  riota2df  5894  eloprabga  6005  frecabcl  6452  mptelixpg  6788  exmidfodomrlemreseldju  7260  enq0breq  7496  genpassl  7584  genpassu  7585  elnnnn0  9283  peano2z  9353  znnsub  9368  znn0sub  9382  uzin  9625  nn01to3  9682  rpnegap  9752  negelrp  9753  xsubge0  9947  divelunit  10068  elfz5  10083  uzsplit  10158  elfzonelfzo  10297  adddivflid  10361  divfl0  10365  2shfti  10975  rexuz3  11134  clim2c  11427  fisumss  11535  infssuzex  12086  bezoutlemmain  12135  nninfctlemfo  12177  pc2dvds  12468  1arith  12505  xpsfrnel  12927  xpsfrnel2  12929  ghmeqker  13341  lsslss  13877  zndvds  14137  znleval2  14142  eltg3  14225  lmbrf  14383  cnrest2  14404  cnptoprest  14407  cnptoprest2  14408  ismet2  14522  elbl2ps  14560  elbl2  14561  xblpnfps  14566  xblpnf  14567  bdxmet  14669  metcn  14682  cnbl0  14702  cnblcld  14703  mulc1cncf  14744  ellimc3apf  14814  pilem1  14914  wilthlem1  15112  lgsdilem  15143  lgsne0  15154  lgsabs1  15155  lgsquadlem1  15191