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  1065  cad1  1608  raldifeq  4437  rexreusng  4611  posn  5631  elrnmpt1  5824  dfres3  5852  opelres  5853  fliftf  7057  eroveu  8382  ixpfi2  8811  elfi2  8867  dffi3  8884  cfss  9676  wunex2  10149  nnle1eq1  11656  nn0le0eq0  11914  ixxun  12744  ioopos  12803  injresinj  13148  hashle00  13751  prprrab  13821  xpcogend  14324  cnpart  14589  fz1f1o  15057  nndivdvds  15606  dvdsmultr2  15639  bitsmod  15775  sadadd  15806  sadass  15810  smuval2  15821  smumul  15832  pcmpt  16218  pcmpt2  16219  prmreclem2  16243  prmreclem5  16246  ramcl  16355  mrcidb2  16879  acsfn  16920  fncnvimaeqv  17360  latleeqj1  17663  resmndismnd  17963  pgpssslw  18670  subgdmdprd  19087  acsfn1p  19509  lssle0  19652  islpir2  19954  islinds3  20908  iscld4  21603  cncnpi  21816  cnprest2  21828  lmss  21836  isconn2  21952  dfconn2  21957  subislly  22019  lly1stc  22034  elptr  22111  txcn  22164  xkoinjcn  22225  tsmsres  22681  isxmet2d  22866  xmetgt0  22897  prdsxmetlem  22907  imasdsf1olem  22912  xblss2  22941  stdbdbl  23056  prdsxmslem2  23068  xrtgioo  23343  xrsxmet  23346  cnmpopc  23461  elpi1i  23579  minveclem7  23967  elovolmr  24006  ismbf  24158  mbfmax  24179  itg1val2  24214  mbfi1fseqlem4  24248  itgresr  24308  iblrelem  24320  iblpos  24322  rlimcnp  25471  rlimcnp2  25472  chpchtsum  25723  lgsneg  25825  lgsdilem  25828  2lgslem1a  25895  lmiinv  26506  isspthonpth  27458  s3wwlks2on  27663  clwlkclwwlk  27708  clwwlknonel  27802  clwwlknun  27819  eupth2lem2  27926  frgr3vlem2  27981  numclwwlk2lem1  28083  minvecolem7  28588  shle0  29147  mdsl2bi  30028  dmdbr5ati  30127  cdj3lem1  30139  eulerpartlemr  31532  subfacp1lem3  32327  satefvfmla1  32570  hfext  33542  bj-issetwt  34087  poimirlem25  34799  poimirlem26  34800  poimirlem27  34801  mblfinlem3  34813  mblfinlem4  34814  mbfresfi  34820  itg2addnclem  34825  itg2addnc  34828  heiborlem10  34981  dffunsALTV2  35799  dffunsALTV3  35800  dffunsALTV4  35801  elfunsALTV2  35808  elfunsALTV3  35809  elfunsALTV4  35810  elfunsALTV5  35811  dfdisjs2  35824  dfdisjs5  35827  eldisjs2  35838  ople0  36205  atlle0  36323  cdlemg10c  37657  cdlemg33c  37726  hdmap14lem13  38898  mrefg3  39185  radcnvrat  40526  2ffzoeq  43409
  Copyright terms: Public domain W3C validator