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 ) ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  mpbirand  445  3anibar  1196  3biant1d  1396  drex1  1851  elrab3t  2981  eldifvsn  3847  bnd2  4312  opbrop  4856  opelresi  5076  funcnv3  5446  fnssresb  5498  dff1o5  5651  fneqeql2  5821  fnniniseg2  5835  dffo3  5858  fmptco  5877  fnressn  5904  fconst4m  5938  riota2df  6063  eloprabga  6178  suppimacnvfn  6490  mptsuppd  6500  suppssrst  6505  suppssrgst  6506  frecabcl  6675  mptelixpg  7022  relresfin  7270  exmidfodomrlemreseldju  7558  enq0breq  7809  genpassl  7897  genpassu  7898  elnnnn0  9617  peano2z  9689  znnsub  9705  znn0sub  9719  uzin  9970  nn01to3  10032  rpnegap  10103  negelrp  10104  xsubge0  10299  divelunit  10420  elfz5  10436  uzsplit  10515  elfzonelfzo  10664  infssuzex  10682  adddivflid  10747  divfl0  10751  hashfibclem  11303  hashf1lem1  11306  swrdspsleq  11460  2shfti  11617  rexuz3  11777  clim2c  12074  fisumss  12183  bitsmod  12747  bitscmp  12749  bezoutlemmain  12799  nninfctlemfo  12841  dvdsfi  13045  pc2dvds  13137  1arith  13174  xpsfrnel  13723  xpsfrnel2  13725  ghmeqker  14132  lsslss  14826  zndvds  15092  znleval2  15097  eltg3  15300  lmbrf  15458  cnrest2  15479  cnptoprest  15482  cnptoprest2  15483  ismet2  15597  elbl2ps  15635  elbl2  15636  xblpnfps  15641  xblpnf  15642  bdxmet  15744  metcn  15757  cnbl0  15777  cnblcld  15778  mulc1cncf  15832  ellimc3apf  15903  pilem1  16023  wilthlem1  16249  bposlem1  16328  lgsdilem  16368  lgsne0  16379  lgsabs1  16380  lgsquadlem1  16418  lgsquadlem2  16419  isclwwlknx  16879  clwwlkn1  16881