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  4310  opbrop  4854  opelresi  5074  funcnv3  5443  fnssresb  5495  dff1o5  5648  fneqeql2  5818  fnniniseg2  5832  dffo3  5855  fmptco  5874  fnressn  5901  fconst4m  5935  riota2df  6060  eloprabga  6175  suppimacnvfn  6486  mptsuppd  6496  suppssrst  6501  suppssrgst  6502  frecabcl  6670  mptelixpg  7016  exmidfodomrlemreseldju  7552  enq0breq  7803  genpassl  7891  genpassu  7892  elnnnn0  9606  peano2z  9680  znnsub  9696  znn0sub  9710  uzin  9955  nn01to3  10017  rpnegap  10087  negelrp  10088  xsubge0  10283  divelunit  10404  elfz5  10420  uzsplit  10499  elfzonelfzo  10648  infssuzex  10666  adddivflid  10727  divfl0  10731  hashfibclem  11282  hashf1lem1  11285  swrdspsleq  11439  2shfti  11596  rexuz3  11756  clim2c  12050  fisumss  12159  bitsmod  12723  bitscmp  12725  bezoutlemmain  12775  nninfctlemfo  12817  dvdsfi  13017  pc2dvds  13109  1arith  13146  xpsfrnel  13665  xpsfrnel2  13667  ghmeqker  14074  lsslss  14718  zndvds  14984  znleval2  14989  eltg3  15158  lmbrf  15316  cnrest2  15337  cnptoprest  15340  cnptoprest2  15341  ismet2  15455  elbl2ps  15493  elbl2  15494  xblpnfps  15499  xblpnf  15500  bdxmet  15602  metcn  15615  cnbl0  15635  cnblcld  15636  mulc1cncf  15690  ellimc3apf  15761  pilem1  15880  wilthlem1  16094  lgsdilem  16146  lgsne0  16157  lgsabs1  16158  lgsquadlem1  16196  lgsquadlem2  16197  isclwwlknx  16657  clwwlkn1  16659