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  1165  drex1  1798  elrab3t  2892  bnd2  4171  opbrop  4703  opelresi  4915  funcnv3  5275  fnssresb  5325  dff1o5  5467  fneqeql2  5622  fnniniseg2  5636  rexsupp  5637  dffo3  5660  fmptco  5679  fnressn  5699  fconst4m  5733  riota2df  5846  eloprabga  5957  frecabcl  6395  mptelixpg  6729  exmidfodomrlemreseldju  7194  enq0breq  7430  genpassl  7518  genpassu  7519  elnnnn0  9213  peano2z  9283  znnsub  9298  znn0sub  9312  uzin  9554  nn01to3  9611  rpnegap  9680  negelrp  9681  xsubge0  9875  divelunit  9996  elfz5  10010  uzsplit  10085  elfzonelfzo  10223  adddivflid  10285  divfl0  10289  2shfti  10831  rexuz3  10990  clim2c  11283  fisumss  11391  infssuzex  11940  bezoutlemmain  11989  pc2dvds  12319  1arith  12355  eltg3  13339  lmbrf  13497  cnrest2  13518  cnptoprest  13521  cnptoprest2  13522  ismet2  13636  elbl2ps  13674  elbl2  13675  xblpnfps  13680  xblpnf  13681  bdxmet  13783  metcn  13796  cnbl0  13816  cnblcld  13817  mulc1cncf  13858  ellimc3apf  13911  pilem1  13982  lgsdilem  14210  lgsne0  14221  lgsabs1  14222