MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  biantrud Structured version   Visualization version   GIF version

Theorem biantrud 532
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
StepHypRef Expression
1 biantrud.1 . 2 (𝜑𝜓)
2 iba 528 . 2 (𝜓 → (𝜒 ↔ (𝜒𝜓)))
31, 2syl 17 1 (𝜑 → (𝜒 ↔ (𝜒𝜓)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396
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 208  df-an 397
This theorem is referenced by:  ifptru  1067  cad1  1610  raldifeq  4442  rexreusng  4616  posn  5636  elrnmpt1  5829  dfres3  5857  opelres  5858  fliftf  7062  eroveu  8387  ixpfi2  8816  elfi2  8872  dffi3  8889  cfss  9681  wunex2  10154  nnle1eq1  11661  nn0le0eq0  11919  ixxun  12749  ioopos  12808  injresinj  13153  hashle00  13756  prprrab  13826  xpcogend  14329  cnpart  14594  fz1f1o  15062  nndivdvds  15611  dvdsmultr2  15644  bitsmod  15780  sadadd  15811  sadass  15815  smuval2  15826  smumul  15837  pcmpt  16223  pcmpt2  16224  prmreclem2  16248  prmreclem5  16251  ramcl  16360  mrcidb2  16884  acsfn  16925  fncnvimaeqv  17365  latleeqj1  17668  resmndismnd  17968  pgpssslw  18675  subgdmdprd  19092  acsfn1p  19514  lssle0  19657  islpir2  19959  islinds3  20913  iscld4  21608  cncnpi  21821  cnprest2  21833  lmss  21841  isconn2  21957  dfconn2  21962  subislly  22024  lly1stc  22039  elptr  22116  txcn  22169  xkoinjcn  22230  tsmsres  22686  isxmet2d  22871  xmetgt0  22902  prdsxmetlem  22912  imasdsf1olem  22917  xblss2  22946  stdbdbl  23061  prdsxmslem2  23073  xrtgioo  23348  xrsxmet  23351  cnmpopc  23466  elpi1i  23584  minveclem7  23972  elovolmr  24011  ismbf  24163  mbfmax  24184  itg1val2  24219  mbfi1fseqlem4  24253  itgresr  24313  iblrelem  24325  iblpos  24327  rlimcnp  25476  rlimcnp2  25477  chpchtsum  25728  lgsneg  25830  lgsdilem  25833  2lgslem1a  25900  lmiinv  26511  isspthonpth  27463  s3wwlks2on  27668  clwlkclwwlk  27713  clwwlknonel  27807  clwwlknun  27824  eupth2lem2  27931  frgr3vlem2  27986  numclwwlk2lem1  28088  minvecolem7  28593  shle0  29152  mdsl2bi  30033  dmdbr5ati  30132  cdj3lem1  30144  eulerpartlemr  31537  subfacp1lem3  32332  satefvfmla1  32575  hfext  33547  bj-issetwt  34092  poimirlem25  34803  poimirlem26  34804  poimirlem27  34805  mblfinlem3  34817  mblfinlem4  34818  mbfresfi  34824  itg2addnclem  34829  itg2addnc  34832  heiborlem10  34985  dffunsALTV2  35803  dffunsALTV3  35804  dffunsALTV4  35805  elfunsALTV2  35812  elfunsALTV3  35813  elfunsALTV4  35814  elfunsALTV5  35815  dfdisjs2  35828  dfdisjs5  35831  eldisjs2  35842  ople0  36209  atlle0  36327  cdlemg10c  37661  cdlemg33c  37730  hdmap14lem13  38902  mrefg3  39189  radcnvrat  40530  2ffzoeq  43413
  Copyright terms: Public domain W3C validator