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

This theorem is referenced by:  ifptru  1075  cad1  1617  raldifeq  4494  rexreusng  4679  posn  5771  dmxp  5939  elrnmpt1  5971  dfres3  6002  opelres  6003  ffrnbd  6751  fliftf  7335  eroveu  8852  ixpfi2  9390  elfi2  9454  dffi3  9471  cfss  10305  wunex2  10778  nnle1eq1  12296  nn0le0eq0  12554  ixxun  13403  ioopos  13464  injresinj  13827  hashle00  14439  prprrab  14512  xpcogend  15013  cnpart  15279  fz1f1o  15746  nndivdvds  16299  dvdsmultr2  16335  bitsmod  16473  sadadd  16504  sadass  16508  smuval2  16519  smumul  16530  pcmpt  16930  pcmpt2  16931  prmreclem2  16955  prmreclem5  16958  ramcl  17067  mrcidb2  17661  acsfn  17702  fncnvimaeqv  18164  latleeqj1  18496  resmndismnd  18821  pgpssslw  19632  subgdmdprd  20054  resrhm2b  20602  acsfn1p  20800  lssle0  20948  islpir2  21340  islinds3  21854  iscld4  23073  cncnpi  23286  cnprest2  23298  lmss  23306  isconn2  23422  dfconn2  23427  subislly  23489  lly1stc  23504  elptr  23581  txcn  23634  xkoinjcn  23695  tsmsres  24152  isxmet2d  24337  xmetgt0  24368  prdsxmetlem  24378  imasdsf1olem  24383  xblss2  24412  stdbdbl  24530  prdsxmslem2  24542  xrtgioo  24828  xrsxmet  24831  cnmpopc  24955  elpi1i  25079  minveclem7  25469  elovolmr  25511  ismbf  25663  mbfmax  25684  itg1val2  25719  mbfi1fseqlem4  25753  itgresr  25814  iblrelem  25826  iblpos  25828  rlimcnp  27008  rlimcnp2  27009  chpchtsum  27263  lgsneg  27365  lgsdilem  27368  2lgslem1a  27435  eqscut2  27851  n0subs  28360  lmiinv  28800  isspthonpth  29769  s3wwlks2on  29976  clwlkclwwlk  30021  clwwlknonel  30114  clwwlknun  30131  eupth2lem2  30238  frgr3vlem2  30293  numclwwlk2lem1  30395  nrt2irr  30492  minvecolem7  30902  shle0  31461  mdsl2bi  32342  dmdbr5ati  32441  cdj3lem1  32453  qsfld  33526  eulerpartlemr  34376  subfacp1lem3  35187  satefvfmla1  35430  hfext  36184  bj-issetwt  36876  poimirlem25  37652  poimirlem26  37653  poimirlem27  37654  mblfinlem3  37666  mblfinlem4  37667  mbfresfi  37673  itg2addnclem  37678  itg2addnc  37681  heiborlem10  37827  relssinxpdmrn  38350  dffunsALTV2  38685  dffunsALTV3  38686  dffunsALTV4  38687  elfunsALTV2  38694  elfunsALTV3  38695  elfunsALTV4  38696  elfunsALTV5  38697  dfdisjs2  38710  dfdisjs5  38713  eldisjs2  38724  ople0  39188  atlle0  39306  cdlemg10c  40641  cdlemg33c  40710  hdmap14lem13  41882  mrefg3  42719  onsupneqmaxlim0  43236  onsupnmax  43240  radcnvrat  44333  2ffzoeq  47339