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

Theorem biantrud 527
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 523 . 2 (𝜓 → (𝜒 ↔ (𝜒𝜓)))
31, 2syl 17 1 (𝜑 → (𝜒 ↔ (𝜒𝜓)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384
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 198  df-an 385
This theorem is referenced by:  mpbiran2d  699  ifptru  1096  cad1  1725  raldifeq  4220  posn  5359  elrnmpt1  5545  dfres3  5572  opelres  5573  fliftf  6761  eroveu  8050  ixpfi2  8475  funsnfsupp  8510  elfi2  8531  dffi3  8548  cfss  9344  wunex2  9817  nn2ge  11306  nnle1eq1  11309  nn0le0eq0  11572  ixxun  12398  ioopos  12457  injresinj  12802  hashle00  13394  prprrab  13461  xpcogend  14014  cnpart  14279  fz1f1o  14740  nndivdvds  15288  dvdsmultr2  15320  bitsmod  15453  sadadd  15484  sadass  15488  smuval2  15499  smumul  15510  pcmpt  15889  pcmpt2  15890  prmreclem2  15914  prmreclem5  15917  ramcl  16026  mrcidb2  16558  acsfn  16599  fncnvimaeqv  17039  latleeqj1  17343  pgpssslw  18307  subgdmdprd  18714  lssle0  19233  islpir2  19539  islinds3  20463  iscld4  21163  discld  21187  cncnpi  21376  cnprest2  21388  lmss  21396  isconn2  21511  dfconn2  21516  subislly  21578  lly1stc  21593  elptr  21670  txcn  21723  xkoinjcn  21784  tsmsres  22240  isxmet2d  22425  xmetgt0  22456  prdsxmetlem  22466  imasdsf1olem  22471  xblss2  22500  stdbdbl  22615  prdsxmslem2  22627  xrtgioo  22902  xrsxmet  22905  cncffvrn  22994  cnmpt2pc  23020  elpi1i  23138  minveclem7  23509  elovolmr  23548  ismbf  23700  mbfmax  23721  itg1val2  23756  mbfi1fseqlem4  23790  itgresr  23850  iblrelem  23862  iblpos  23864  itgfsum  23898  rlimcnp  24997  rlimcnp2  24998  chpchtsum  25249  dchreq  25288  lgsneg  25351  lgsdilem  25354  lgsquadlem2  25411  2lgslem1a  25421  lmiinv  25989  isspthonpth  26955  s3wwlks2on  27198  clwlkclwwlk  27247  clwlkclwwlkOLD  27248  clwwlknonel  27385  clwwlknun  27404  clwwlknunOLD  27409  dfconngr1  27484  eupth2lem2  27516  frgr3vlem2  27575  numclwwlk2lem1  27701  numclwwlk2lem1OLD  27712  minvecolem7  28216  shle0  28778  mdsl2bi  29659  dmdbr5ati  29758  cdj3lem1  29770  eulerpartlemr  30904  subfacp1lem3  31633  hfext  32755  bj-issetwt  33305  poimirlem25  33879  poimirlem26  33880  poimirlem27  33881  mblfinlem3  33893  mblfinlem4  33894  mbfresfi  33900  itg2addnclem  33905  itg2addnc  33908  cover2  33952  heiborlem10  34062  ople0  35164  atlle0  35282  cdlemg10c  36616  cdlemg33c  36685  hdmap14lem13  37857  mrefg3  37973  acsfn1p  38470  radcnvrat  39211  2ffzoeq  42096
  Copyright terms: Public domain W3C validator