Theorem biantrud 535

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  ifptru  1075  cad1  1623  raldifeq  4390  rexreusng  4580  posn  5618  elrnmpt1  5811  dfres3  5840  opelres  5841  ffrnbd  6531  fliftf  7094  eroveu  8436  ixpfi2  8908  elfi2  8964  dffi3  8981  cfss  9778  wunex2  10251  nnle1eq1  11759  nn0le0eq0  12017  ixxun  12850  ioopos  12911  injresinj  13262  hashle00  13866  prprrab  13938  xpcogend  14436  cnpart  14702  fz1f1o  15173  nndivdvds  15721  dvdsmultr2  15756  bitsmod  15892  sadadd  15923  sadass  15927  smuval2  15938  smumul  15949  pcmpt  16341  pcmpt2  16342  prmreclem2  16366  prmreclem5  16369  ramcl  16478  mrcidb2  17005  acsfn  17046  fncnvimaeqv  17499  latleeqj1  17802  resmndismnd  18102  pgpssslw  18870  subgdmdprd  19288  acsfn1p  19710  lssle0  19853  islpir2  20156  islinds3  20663  iscld4  21829  cncnpi  22042  cnprest2  22054  lmss  22062  isconn2  22178  dfconn2  22183  subislly  22245  lly1stc  22260  elptr  22337  txcn  22390  xkoinjcn  22451  tsmsres  22908  isxmet2d  23093  xmetgt0  23124  prdsxmetlem  23134  imasdsf1olem  23139  xblss2  23168  stdbdbl  23283  prdsxmslem2  23295  xrtgioo  23571  xrsxmet  23574  cnmpopc  23693  elpi1i  23811  minveclem7  24200  elovolmr  24241  ismbf  24393  mbfmax  24414  itg1val2  24449  mbfi1fseqlem4  24484  itgresr  24544  iblrelem  24556  iblpos  24558  rlimcnp  25716  rlimcnp2  25717  chpchtsum  25968  lgsneg  26070  lgsdilem  26073  2lgslem1a  26140  lmiinv  26751  isspthonpth  27703  s3wwlks2on  27907  clwlkclwwlk  27952  clwwlknonel  28045  clwwlknun  28062  eupth2lem2  28169  frgr3vlem2  28224  numclwwlk2lem1  28326  minvecolem7  28831  shle0  29390  mdsl2bi  30271  dmdbr5ati  30370  cdj3lem1  30382  eulerpartlemr  31924  subfacp1lem3  32728  satefvfmla1  32971  eqscut2  33656  hfext  34141  bj-issetwt  34715  poimirlem25  35458  poimirlem26  35459  poimirlem27  35460  mblfinlem3  35472  mblfinlem4  35473  mbfresfi  35479  itg2addnclem  35484  itg2addnc  35487  heiborlem10  35634  dffunsALTV2  36451  dffunsALTV3  36452  dffunsALTV4  36453  elfunsALTV2  36460  elfunsALTV3  36461  elfunsALTV4  36462  elfunsALTV5  36463  dfdisjs2  36476  dfdisjs5  36479  eldisjs2  36490  ople0  36857  atlle0  36975  cdlemg10c  38309  cdlemg33c  38378  hdmap14lem13  39550  mrefg3  40143  radcnvrat  41511  2ffzoeq  44402