Theorem biantrurd 529

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 525	. 2 |- ( ps -> ( ch <-> ( ps /\ ch ) ) )
3	1, 2	syl 17	1 |- ( ph -> ( ch <-> ( ps /\ ch ) ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386

This theorem is referenced by:  mpbirand  530  3biant1d  1441  elrab3t  3362  n0moeu  3937  eldifvsn  4326  reuxfrd  4893  xpco  5675  funcnv3  5959  fnssresb  6003  dff1o5  6146  fneqeql2  6326  dffo3  6374  fmptco  6396  fconst4  6478  riota2df  6631  eloprabga  6747  fnwelem  7292  mptsuppd  7318  mptelixpg  7945  boxcutc  7951  inficl  8331  wemapso2lem  8457  cantnfle  8568  cantnflem1  8586  bnd2  8756  iscard2  8802  alephinit  8918  kmlem2  8973  cfss  9087  fpwwe2lem9  9460  axgroth2  9647  elnnnn0  11336  znnsub  11423  znn0sub  11424  uzin  11720  negelrp  11864  xsubge0  12091  supxrre1  12160  ixxun  12191  divelunit  12314  elfz5  12334  uzsplit  12412  preduz  12461  injresinj  12589  adddivflid  12619  divfl0  12625  hashf1lem1  13239  swrdspsleq  13449  repswsymball  13526  repswsymballbi  13527  2shfti  13820  cnpart  13980  sqrtneglem  14007  rexuz3  14088  rlim  14226  rlim2  14227  clim2c  14236  ello12  14247  elo12  14258  fsumss  14456  fsumcom2OLD  14506  cvgcmp  14548  fprodss  14678  fprodcom2OLD  14715  bitsmod  15158  bitscmp  15160  pc2dvds  15583  prmreclem4  15623  1arith  15631  ramval  15712  imasleval  16201  xpsfrnel  16223  xpsfrnel2  16225  dfiso2  16432  latleeqm1  17079  latnlemlt  17084  latnle  17085  pospropd  17134  ipole  17158  gsumval2a  17279  ghmeqker  17687  gastacos  17743  isslw  18023  slwpss  18027  pgpssslw  18029  fislw  18040  sylow3lem6  18047  dprd2d2  18443  lsslss  18961  lspsnel5  18995  lsmspsn  19084  coe1mul2lem1  19637  zndvds  19898  znleval2  19904  elfilspd  20142  islinds2  20152  islindf2  20153  eltg3  20766  leordtvallem1  21014  leordtvallem2  21015  lmbrf  21064  cnrest2  21090  cnprest  21093  cnprest2  21094  cnt0  21150  1stccn  21266  kgencn  21359  xkoccn  21422  qtopcn  21517  ordthmeolem  21604  isfbas  21633  fbunfip  21673  fixufil  21726  fbflim  21780  isflf  21797  cnflf  21806  fclscf  21829  cnfcf  21846  alexsubALTlem4  21854  ismet2  22138  elbl2ps  22194  elbl2  22195  xblpnfps  22200  xblpnf  22201  metcn  22348  txmetcn  22353  blval2  22367  metuel2  22370  dscopn  22378  cnbl0  22577  cnblcld  22578  xrtgioo  22609  mulc1cncf  22708  isclmp  22897  isncvsngp  22949  lmmbrf  23060  iscauf  23078  caucfil  23081  lmclim  23101  lmclimf  23102  evthicc2  23229  ovolfioo  23236  ovolficc  23237  ovoliun  23273  ismbl2  23295  volsup  23324  ioombl1lem4  23329  ismbf  23397  ismbfcn  23398  mbfmulc2lem  23414  mbfmax  23416  mbfposr  23419  ismbf3d  23421  mbfimaopnlem  23422  mbfaddlem  23427  mbfsup  23431  i1fpos  23473  mbfi1fseqlem4  23485  xrge0f  23498  itg2seq  23509  itg2monolem1  23517  itg2gt0  23527  itg2cnlem1  23528  itg2cnlem2  23529  i1fibl  23574  ditgneg  23621  lhop1  23777  fta1  24063  ulm2  24139  pilem1  24205  sineq0  24273  ellogrn  24306  rlimcnp  24692  wilthlem1  24794  sqff1o  24908  logfaclbnd  24947  bposlem1  25009  lgsdilem  25049  lgsabs1  25061  lgsdchrval  25079  lgsquadlem1  25105  lgsquadlem2  25106  iscgrgd  25408  trgcgrg  25410  tgellng  25448  ltgov  25492  ishlg  25497  lnhl  25510  israg  25592  islnopp  25631  iscgra  25701  isinag  25729  isleag  25733  iseqlg  25747  ttgelitv  25763  nbupgrel  26241  isuvtxa  26295  iscplgredg  26313  rusgrnumwwlkl1  26863  isclwwlksnx  26889  clwlkclwwlk2  26904  numclwlk1lem2f1  27227  nmoo0  27646  ubthlem1  27726  ch0pss  28304  pjnorm2  28586  adjval  28749  leop  28982  atcv0eq  29238  reuxfr4d  29330  xppreima  29449  fmptcof2  29457  xrdifh  29542  isinftm  29735  smatrcl  29862  ismntoplly  30069  ismntop  30070  brfae  30311  eulerpartlemr  30436  eulerpartlemn  30443  reprinrn  30696  reprinfz1  30700  reprdifc  30705  bnj1173  31070  subfacp1lem5  31166  etasslt  31920  filnetlem4  32376  taupilem3  33165  topdifinffinlem  33195  finxpsuclem  33234  matunitlindf  33407  poimirlem22  33431  poimirlem26  33435  poimirlem27  33436  heicant  33444  mbfposadd  33457  itg2addnclem  33461  itg2addnclem2  33462  iblabsnclem  33473  ftc1anclem1  33485  ftc1anclem5  33489  areacirclem5  33504  areacirc  33505  lmclim2  33554  caures  33556  rrnheibor  33636  isdmn3  33873  opelvvdif  34023  lrelat  34301  lcvbr  34308  lsatcv0eq  34334  ellkr2  34378  lkr0f  34381  lkreqN  34457  opltn0  34477  op1le  34479  leatb  34579  atlltn0  34593  hlrelat5N  34687  hlrelat  34688  cvrval5  34701  cvrexchlem  34705  atcvr0eq  34712  athgt  34742  1cvrco  34758  islpln5  34821  islvol5  34865  elpadd2at2  35093  cdleme0ex2N  35511  cdleme3  35524  cdleme7  35536  cdlemg33e  35998  dochfln0  36766  lcfl1  36781  lcfls1N  36824  lspindp5  37059  isnacs2  37269  rabrenfdioph  37378  rmxycomplete  37482  expdioph  37590  pwfi2f1o  37666  islnr3  37685  isdomn3  37782  ntrneixb  38393  dffo3f  39364  clim2cf  39882  pfxsuffeqwrdeq  41406  oddm1evenALTV  41586  oddp1evenALTV  41587  divgcdoddALTV  41593  ismhm0  41805  isrnghmmul  41893  lco0  42216  lindslinindsimp2lem5  42251  snlindsntor  42260  elbigo2  42346