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  1192  3biant1d  1392  drex1  1847  elrab3t  2975  eldifvsn  3831  bnd2  4291  opbrop  4834  opelresi  5054  funcnv3  5423  fnssresb  5475  dff1o5  5628  fneqeql2  5792  fnniniseg2  5806  dffo3  5829  fmptco  5848  fnressn  5875  fconst4m  5909  riota2df  6033  eloprabga  6148  suppimacnvfn  6459  mptsuppd  6469  suppssrst  6474  suppssrgst  6475  frecabcl  6643  mptelixpg  6982  exmidfodomrlemreseldju  7516  enq0breq  7767  genpassl  7855  genpassu  7856  elnnnn0  9556  peano2z  9630  znnsub  9646  znn0sub  9660  uzin  9905  nn01to3  9967  rpnegap  10037  negelrp  10038  xsubge0  10233  divelunit  10354  elfz5  10370  uzsplit  10448  elfzonelfzo  10597  infssuzex  10615  adddivflid  10676  divfl0  10680  hashfibclem  11231  swrdspsleq  11384  2shfti  11541  rexuz3  11700  clim2c  11994  fisumss  12103  bitsmod  12667  bitscmp  12669  bezoutlemmain  12719  nninfctlemfo  12761  dvdsfi  12961  pc2dvds  13053  1arith  13090  xpsfrnel  13608  xpsfrnel2  13610  ghmeqker  14024  lsslss  14655  zndvds  14923  znleval2  14928  eltg3  15048  lmbrf  15206  cnrest2  15227  cnptoprest  15230  cnptoprest2  15231  ismet2  15345  elbl2ps  15383  elbl2  15384  xblpnfps  15389  xblpnf  15390  bdxmet  15492  metcn  15505  cnbl0  15525  cnblcld  15526  mulc1cncf  15580  ellimc3apf  15651  pilem1  15770  wilthlem1  15974  lgsdilem  16026  lgsne0  16037  lgsabs1  16038  lgsquadlem1  16076  lgsquadlem2  16077  isclwwlknx  16537  clwwlkn1  16539