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

Theorem biantrud 509
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  |-  ( ph  ->  ps )
Assertion
Ref Expression
biantrud  |-  ( ph  ->  ( ch  <->  ( ch  /\ 
ps ) ) )

Proof of Theorem biantrud
StepHypRef Expression
1 biantrud.1 . 2  |-  ( ph  ->  ps )
2 iba 505 . 2  |-  ( ps 
->  ( ch  <->  ( ch  /\ 
ps ) ) )
31, 2syl 17 1  |-  ( ph  ->  ( ch  <->  ( ch  /\ 
ps ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    /\ wa 370
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 188  df-an 372
This theorem is referenced by:  ifptru  1431  cad1  1514  raldifeq  3891  posn  4923  elrnmpt1  5103  fliftf  6223  eroveu  7466  ixpfi2  7878  funsnfsupp  7913  elfi2  7934  dffi3  7951  cfss  8693  wunex2  9162  nn2ge  10634  nnle1eq1  10637  nn0le0eq0  10898  nn0lt10bOLD  10999  ixxun  11651  ioopos  11711  injresinj  12022  xpcogend  13017  cnpart  13282  fz1f1o  13754  nndivdvds  14289  dvdsmultr2  14318  bitsmod  14384  sadadd  14415  sadass  14419  smuval2  14430  smumul  14441  pcmpt  14800  pcmpt2  14801  prmreclem2  14824  prmreclem5  14827  ramcl  14950  mrcidb2  15475  acsfn  15516  fncnvimaeqv  15956  latleeqj1  16260  pgpssslw  17201  subgdmdprd  17602  lssle0  18108  islpir2  18410  islinds3  19323  iscld4  20012  discld  20036  cncnpi  20225  cnprest2  20237  lmss  20245  iscon2  20360  dfcon2  20365  subislly  20427  lly1stc  20442  elptr  20519  txcn  20572  hauseqlcld  20592  xkoinjcn  20633  tsmsres  21089  isxmet2d  21273  xmetgt0  21304  prdsxmetlem  21314  imasdsf1olem  21319  xblss2  21348  stdbdbl  21463  prdsxmslem2  21475  xrtgioo  21735  xrsxmet  21738  cncffvrn  21826  cnmpt2pc  21852  elpi1i  21970  minveclem7  22270  elovolmr  22307  ismbf  22463  mbfmax  22482  itg1val2  22519  mbfi1fseqlem4  22553  itgresr  22613  iblrelem  22625  iblpos  22627  itgfsum  22661  rlimcnp  23756  rlimcnp2  23757  chpchtsum  24010  dchreq  24049  lgsneg  24110  lgsdilem  24113  lgsquadlem2  24146  lmiinv  24690  isusgra0  24920  usgraop  24923  dfconngra1  25244  eupath2lem2  25551  frgra3vlem2  25574  numclwwlk2lem1  25675  minvecolem7  26370  shle0  26930  mdsl2bi  27811  dmdbr5ati  27910  cdj3lem1  27922  eulerpartlemr  29033  subfacp1lem3  29693  dfres3  30186  hfext  30735  bj-issetwt  31219  poimirlem25  31668  poimirlem26  31669  poimirlem27  31670  mblfinlem3  31682  mblfinlem4  31683  mbfresfi  31690  itg2addnclem  31696  itg2addnc  31699  cover2  31743  heiborlem10  31855  ople0  32461  atlle0  32579  cdlemg10c  33914  cdlemg33c  33983  hdmap14lem13  35159  mrefg3  35258  acsfn1p  35763  radcnvrat  36299  funressnfv  38019  dfdfat2  38022  2ffzoeq  38412
  Copyright terms: Public domain W3C validator