Theorem biantrud 541

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 537	. 2 ⊢ (𝜓 → (𝜒 ↔ (𝜒 ∧ 𝜓)))
3	1, 2	syl 18	1 ⊢ (𝜑 → (𝜒 ↔ (𝜒 ∧ 𝜓)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  ifptru  1091  cad1  1650  nrmod  3843  raldifeq  4452  rexreusng  4640  posn  5742  dmxp  5918  elrnmpt1  5949  dfres3  5986  opelres  5987  ffrnbd  6747  fliftf  7346  eroveu  8861  ixpfi2  9367  elfi2  9433  dffi3  9450  cfss  10370  wunex2  10850  nnle1eq1  12395  nn0le0eq0  12661  ixxun  13519  ioopos  13582  injresinj  13953  hashle00  14571  prprrab  14645  xpcogend  15156  cnpart  15436  fz1f1o  15905  nndivdvds  16460  dvdsmultr2  16497  bitsmod  16635  sadadd  16666  sadass  16670  smuval2  16681  smumul  16692  pcmpt  17099  pcmpt2  17100  prmreclem2  17124  prmreclem5  17127  ramcl  17236  mrcidb2  17821  acsfn  17862  fncnvimaeqv  18323  latleeqj1  18654  resmndismnd  19032  pgpssslw  19858  subgdmdprd  20280  resrhm2b  20884  acsfn1p  21086  lssle0  21255  islpir2  21684  islinds3  22170  iscld4  23413  cncnpi  23626  cnprest2  23638  lmss  23646  isconn2  23762  dfconn2  23767  subislly  23830  lly1stc  23845  elptr  23922  txcn  23975  xkoinjcn  24036  tsmsres  24493  isxmet2d  24676  xmetgt0  24707  prdsxmetlem  24717  imasdsf1olem  24722  xblss2  24751  stdbdbl  24866  prdsxmslem2  24878  xrtgioo  25156  xrsxmet  25159  cnmpopc  25279  elpi1i  25397  minveclem7  25786  elovolmr  25827  ismbf  25979  mbfmax  26000  itg1val2  26035  mbfi1fseqlem4  26069  itgresr  26129  iblrelem  26141  iblpos  26143  rlimcnp  27323  rlimcnp2  27324  chpchtsum  27576  lgsneg  27678  lgsdilem  27681  2lgslem1a  27748  eqcuts2  28202  n0subs  28779  n0lts1e0  28784  zsoring  28825  bdaypw2n0bndlem  28879  lmiinv  29327  isspthonpth  30365  s3wwlks2on  30575  sps3wwlks2on  30576  clwlkclwwlk  30623  clwwlknonel  30716  clwwlknun  30733  eupth2lem2  30850  frgr3vlem2  30905  numclwwlk2lem1  31007  nrt2irr  31104  minvecolem7  31515  shle0  32074  mdsl2bi  32955  dmdbr5ati  33054  cdj3lem1  33066  rlocisunit  33907  qsfld  34092  eulerpartlemr  35076  subfacp1lem3  36114  satefvfmla1  36357  hfext  37112  bj-issetwt  37965  poimirlem25  38755  poimirlem26  38756  poimirlem27  38757  mblfinlem3  38769  mblfinlem4  38770  mbfresfi  38776  itg2addnclem  38781  itg2addnc  38784  heiborlem10  38946  relssinxpdmrn  39473  dffunsALTV2  39893  dffunsALTV3  39894  dffunsALTV4  39895  elfunsALTV2  39902  elfunsALTV3  39903  elfunsALTV4  39904  elfunsALTV5  39905  dfdisjs2  39918  dfdisjs5  39921  disjimdmqseq  39933  eldisjs2  39944  ople0  40436  atlle0  40554  cdlemg10c  41888  cdlemg33c  41957  hdmap14lem13  43129  mrefg3  43912  onsupneqmaxlim0  44418  onsupnmax  44422  radcnvrat  45490  2ffzoeq  48603