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  1189  3biant1d  1389  drex1  1844  elrab3t  2958  bnd2  4257  opbrop  4798  opelresi  5016  funcnv3  5383  fnssresb  5435  dff1o5  5581  fneqeql2  5744  fnniniseg2  5758  rexsupp  5759  dffo3  5782  fmptco  5801  fnressn  5825  fconst4m  5859  riota2df  5976  eloprabga  6091  frecabcl  6545  mptelixpg  6881  exmidfodomrlemreseldju  7378  enq0breq  7623  genpassl  7711  genpassu  7712  elnnnn0  9412  peano2z  9482  znnsub  9498  znn0sub  9512  uzin  9755  nn01to3  9812  rpnegap  9882  negelrp  9883  xsubge0  10077  divelunit  10198  elfz5  10213  uzsplit  10288  elfzonelfzo  10436  infssuzex  10453  adddivflid  10512  divfl0  10516  swrdspsleq  11199  2shfti  11342  rexuz3  11501  clim2c  11795  fisumss  11903  bitsmod  12467  bitscmp  12469  bezoutlemmain  12519  nninfctlemfo  12561  dvdsfi  12761  pc2dvds  12853  1arith  12890  xpsfrnel  13377  xpsfrnel2  13379  ghmeqker  13808  lsslss  14345  zndvds  14613  znleval2  14618  eltg3  14731  lmbrf  14889  cnrest2  14910  cnptoprest  14913  cnptoprest2  14914  ismet2  15028  elbl2ps  15066  elbl2  15067  xblpnfps  15072  xblpnf  15073  bdxmet  15175  metcn  15188  cnbl0  15208  cnblcld  15209  mulc1cncf  15263  ellimc3apf  15334  pilem1  15453  wilthlem1  15654  lgsdilem  15706  lgsne0  15717  lgsabs1  15718  lgsquadlem1  15756  lgsquadlem2  15757