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  1846  elrab3t  2962  eldifvsn  3810  bnd2  4269  opbrop  4811  opelresi  5030  funcnv3  5399  fnssresb  5451  dff1o5  5601  fneqeql2  5765  fnniniseg2  5779  dffo3  5802  fmptco  5821  fnressn  5848  fconst4m  5882  riota2df  6003  eloprabga  6118  suppimacnvfn  6424  mptsuppd  6434  suppssrst  6439  suppssrgst  6440  frecabcl  6608  mptelixpg  6946  exmidfodomrlemreseldju  7471  enq0breq  7716  genpassl  7804  genpassu  7805  elnnnn0  9504  peano2z  9576  znnsub  9592  znn0sub  9606  uzin  9850  nn01to3  9912  rpnegap  9982  negelrp  9983  xsubge0  10177  divelunit  10298  elfz5  10314  uzsplit  10389  elfzonelfzo  10538  infssuzex  10556  adddivflid  10615  divfl0  10619  swrdspsleq  11314  2shfti  11471  rexuz3  11630  clim2c  11924  fisumss  12033  bitsmod  12597  bitscmp  12599  bezoutlemmain  12649  nninfctlemfo  12691  dvdsfi  12891  pc2dvds  12983  1arith  13020  xpsfrnel  13507  xpsfrnel2  13509  ghmeqker  13938  lsslss  14477  zndvds  14745  znleval2  14750  eltg3  14868  lmbrf  15026  cnrest2  15047  cnptoprest  15050  cnptoprest2  15051  ismet2  15165  elbl2ps  15203  elbl2  15204  xblpnfps  15209  xblpnf  15210  bdxmet  15312  metcn  15325  cnbl0  15345  cnblcld  15346  mulc1cncf  15400  ellimc3apf  15471  pilem1  15590  wilthlem1  15794  lgsdilem  15846  lgsne0  15857  lgsabs1  15858  lgsquadlem1  15896  lgsquadlem2  15897  isclwwlknx  16357  clwwlkn1  16359