Theorem biantrud 531

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	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
biantrud	⊢ (𝜑 → (𝜒 ↔ (𝜒 ∧ 𝜓)))

Proof of Theorem biantrud

Step	Hyp	Ref	Expression
1		biantrud.1	. 2 ⊢ (𝜑 → 𝜓)
2		iba 527	. 2 ⊢ (𝜓 → (𝜒 ↔ (𝜒 ∧ 𝜓)))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝜒 ↔ (𝜒 ∧ 𝜓)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395

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 206  df-an 396

This theorem is referenced by:  ifptru  1073  cad1  1611  raldifeq  4494  rexreusng  4684  posn  5763  elrnmpt1  5960  dfres3  5990  opelres  5991  ffrnbd  6738  fliftf  7323  eroveu  8830  ixpfi2  9374  elfi2  9437  dffi3  9454  cfss  10288  wunex2  10761  nnle1eq1  12272  nn0le0eq0  12530  ixxun  13372  ioopos  13433  injresinj  13785  hashle00  14391  prprrab  14466  xpcogend  14953  cnpart  15219  fz1f1o  15688  nndivdvds  16239  dvdsmultr2  16274  bitsmod  16410  sadadd  16441  sadass  16445  smuval2  16456  smumul  16467  pcmpt  16860  pcmpt2  16861  prmreclem2  16885  prmreclem5  16888  ramcl  16997  mrcidb2  17597  acsfn  17638  fncnvimaeqv  18109  latleeqj1  18442  resmndismnd  18759  pgpssslw  19568  subgdmdprd  19990  resrhm2b  20540  acsfn1p  20686  lssle0  20833  islpir2  21219  islinds3  21767  iscld4  22968  cncnpi  23181  cnprest2  23193  lmss  23201  isconn2  23317  dfconn2  23322  subislly  23384  lly1stc  23399  elptr  23476  txcn  23529  xkoinjcn  23590  tsmsres  24047  isxmet2d  24232  xmetgt0  24263  prdsxmetlem  24273  imasdsf1olem  24278  xblss2  24307  stdbdbl  24425  prdsxmslem2  24437  xrtgioo  24721  xrsxmet  24724  cnmpopc  24848  elpi1i  24972  minveclem7  25362  elovolmr  25404  ismbf  25556  mbfmax  25577  itg1val2  25612  mbfi1fseqlem4  25647  itgresr  25707  iblrelem  25719  iblpos  25721  rlimcnp  26896  rlimcnp2  26897  chpchtsum  27151  lgsneg  27253  lgsdilem  27256  2lgslem1a  27323  eqscut2  27738  lmiinv  28595  isspthonpth  29562  s3wwlks2on  29766  clwlkclwwlk  29811  clwwlknonel  29904  clwwlknun  29921  eupth2lem2  30028  frgr3vlem2  30083  numclwwlk2lem1  30185  nrt2irr  30282  minvecolem7  30692  shle0  31251  mdsl2bi  32132  dmdbr5ati  32231  cdj3lem1  32243  qsfld  33209  eulerpartlemr  33994  subfacp1lem3  34792  satefvfmla1  35035  hfext  35779  bj-issetwt  36352  poimirlem25  37118  poimirlem26  37119  poimirlem27  37120  mblfinlem3  37132  mblfinlem4  37133  mbfresfi  37139  itg2addnclem  37144  itg2addnc  37147  heiborlem10  37293  relssinxpdmrn  37821  dffunsALTV2  38156  dffunsALTV3  38157  dffunsALTV4  38158  elfunsALTV2  38165  elfunsALTV3  38166  elfunsALTV4  38167  elfunsALTV5  38168  dfdisjs2  38181  dfdisjs5  38184  eldisjs2  38195  ople0  38659  atlle0  38777  cdlemg10c  40112  cdlemg33c  40181  hdmap14lem13  41353  mrefg3  42128  onsupneqmaxlim0  42652  onsupnmax  42656  radcnvrat  43751  2ffzoeq  46708