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  1821  elrab3t  2928  bnd2  4217  opbrop  4754  opelresi  4970  funcnv3  5336  fnssresb  5388  dff1o5  5531  fneqeql2  5689  fnniniseg2  5703  rexsupp  5704  dffo3  5727  fmptco  5746  fnressn  5770  fconst4m  5804  riota2df  5920  eloprabga  6032  frecabcl  6485  mptelixpg  6821  exmidfodomrlemreseldju  7308  enq0breq  7549  genpassl  7637  genpassu  7638  elnnnn0  9338  peano2z  9408  znnsub  9424  znn0sub  9438  uzin  9681  nn01to3  9738  rpnegap  9808  negelrp  9809  xsubge0  10003  divelunit  10124  elfz5  10139  uzsplit  10214  elfzonelfzo  10359  infssuzex  10376  adddivflid  10435  divfl0  10439  swrdspsleq  11120  2shfti  11142  rexuz3  11301  clim2c  11595  fisumss  11703  bitsmod  12267  bitscmp  12269  bezoutlemmain  12319  nninfctlemfo  12361  dvdsfi  12561  pc2dvds  12653  1arith  12690  xpsfrnel  13176  xpsfrnel2  13178  ghmeqker  13607  lsslss  14143  zndvds  14411  znleval2  14416  eltg3  14529  lmbrf  14687  cnrest2  14708  cnptoprest  14711  cnptoprest2  14712  ismet2  14826  elbl2ps  14864  elbl2  14865  xblpnfps  14870  xblpnf  14871  bdxmet  14973  metcn  14986  cnbl0  15006  cnblcld  15007  mulc1cncf  15061  ellimc3apf  15132  pilem1  15251  wilthlem1  15452  lgsdilem  15504  lgsne0  15515  lgsabs1  15516  lgsquadlem1  15554  lgsquadlem2  15555