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  1168  3biant1d  1367  drex1  1822  elrab3t  2935  bnd2  4233  opbrop  4772  opelresi  4989  funcnv3  5355  fnssresb  5407  dff1o5  5553  fneqeql2  5712  fnniniseg2  5726  rexsupp  5727  dffo3  5750  fmptco  5769  fnressn  5793  fconst4m  5827  riota2df  5943  eloprabga  6055  frecabcl  6508  mptelixpg  6844  exmidfodomrlemreseldju  7339  enq0breq  7584  genpassl  7672  genpassu  7673  elnnnn0  9373  peano2z  9443  znnsub  9459  znn0sub  9473  uzin  9716  nn01to3  9773  rpnegap  9843  negelrp  9844  xsubge0  10038  divelunit  10159  elfz5  10174  uzsplit  10249  elfzonelfzo  10396  infssuzex  10413  adddivflid  10472  divfl0  10476  swrdspsleq  11158  2shfti  11257  rexuz3  11416  clim2c  11710  fisumss  11818  bitsmod  12382  bitscmp  12384  bezoutlemmain  12434  nninfctlemfo  12476  dvdsfi  12676  pc2dvds  12768  1arith  12805  xpsfrnel  13291  xpsfrnel2  13293  ghmeqker  13722  lsslss  14258  zndvds  14526  znleval2  14531  eltg3  14644  lmbrf  14802  cnrest2  14823  cnptoprest  14826  cnptoprest2  14827  ismet2  14941  elbl2ps  14979  elbl2  14980  xblpnfps  14985  xblpnf  14986  bdxmet  15088  metcn  15101  cnbl0  15121  cnblcld  15122  mulc1cncf  15176  ellimc3apf  15247  pilem1  15366  wilthlem1  15567  lgsdilem  15619  lgsne0  15630  lgsabs1  15631  lgsquadlem1  15669  lgsquadlem2  15670