Theorem biantrud 528

Description: A wff is equivalent to its conjunction with truth. (Contributed by NM, 2-Aug-1994.) (Proof shortened by Wolf Lammen, 23-Oct-2013.)

Hypothesis

Ref	Expression
biantrud.1	|- ( ph -> ps )

Assertion

Ref	Expression
biantrud	|- ( ph -> ( ch <-> ( ch /\ ps ) ) )

Proof of Theorem biantrud

Step	Hyp	Ref	Expression
1		biantrud.1	. 2 |- ( ph -> ps )
2		iba 524	. 2 |- ( ps -> ( ch <-> ( ch /\ ps ) ) )
3	1, 2	syl 17	1 |- ( ph -> ( ch <-> ( ch /\ ps ) ) )

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:  ifptru  1023  cad1  1555  raldifeq  4059  posn  5187  elrnmpt1  5374  dfres3  5403  fliftf  6565  eroveu  7842  ixpfi2  8264  funsnfsupp  8299  elfi2  8320  dffi3  8337  cfss  9087  wunex2  9560  nn2ge  11045  nnle1eq1  11048  nn0le0eq0  11321  ixxun  12191  ioopos  12250  injresinj  12589  hashle00  13188  prprrab  13255  xpcogend  13713  cnpart  13980  fz1f1o  14441  nndivdvds  14989  dvdsmultr2  15021  bitsmod  15158  sadadd  15189  sadass  15193  smuval2  15204  smumul  15215  pcmpt  15596  pcmpt2  15597  prmreclem2  15621  prmreclem5  15624  ramcl  15733  mrcidb2  16278  acsfn  16320  fncnvimaeqv  16760  latleeqj1  17063  pgpssslw  18029  subgdmdprd  18433  lssle0  18950  islpir2  19251  islinds3  20173  iscld4  20869  discld  20893  cncnpi  21082  cnprest2  21094  lmss  21102  isconn2  21217  dfconn2  21222  subislly  21284  lly1stc  21299  elptr  21376  txcn  21429  hauseqlcld  21449  xkoinjcn  21490  tsmsres  21947  isxmet2d  22132  xmetgt0  22163  prdsxmetlem  22173  imasdsf1olem  22178  xblss2  22207  stdbdbl  22322  prdsxmslem2  22334  xrtgioo  22609  xrsxmet  22612  cncffvrn  22701  cnmpt2pc  22727  elpi1i  22846  minveclem7  23206  elovolmr  23244  ismbf  23397  mbfmax  23416  itg1val2  23451  mbfi1fseqlem4  23485  itgresr  23545  iblrelem  23557  iblpos  23559  itgfsum  23593  rlimcnp  24692  rlimcnp2  24693  chpchtsum  24944  dchreq  24983  lgsneg  25046  lgsdilem  25049  lgsquadlem2  25106  2lgslem1a  25116  lmiinv  25684  isspthonpth  26645  s3wwlks2on  26849  clwlkclwwlk  26903  clwwlksnun  26974  dfconngr1  27048  eupth2lem2  27079  frgr3vlem2  27138  numclwwlk2lem1  27235  minvecolem7  27739  shle0  28301  mdsl2bi  29182  dmdbr5ati  29281  cdj3lem1  29293  eulerpartlemr  30436  subfacp1lem3  31164  hfext  32290  bj-issetwt  32859  poimirlem25  33434  poimirlem26  33435  poimirlem27  33436  mblfinlem3  33448  mblfinlem4  33449  mbfresfi  33456  itg2addnclem  33461  itg2addnc  33464  cover2  33508  heiborlem10  33619  opelresALTV  34031  ople0  34474  atlle0  34592  cdlemg10c  35927  cdlemg33c  35996  hdmap14lem13  37172  mrefg3  37271  acsfn1p  37769  radcnvrat  38513  funressnfv  41208  dfdfat2  41211  2ffzoeq  41338