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

Theorem biantrud 507
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 503 . 2  |-  ( ps 
->  ( ch  <->  ( ch  /\ 
ps ) ) )
31, 2syl 16 1  |-  ( ph  ->  ( ch  <->  ( ch  /\ 
ps ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369
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 185  df-an 371
This theorem is referenced by:  raldifeq  3875  posn  5014  elrnmpt1  5195  fliftf  6116  eroveu  7304  ixpfi2  7719  funsnfsupp  7754  elfi2  7774  dffi3  7791  cantnfrescl  7994  cfss  8544  wunex2  9015  nn2ge  10457  nnle1eq1  10460  nn0le0eq0  10718  nn0lt10b  10816  ixxun  11426  ioopos  11482  injresinj  11755  cnpart  12846  fz1f1o  13304  nndivdvds  13658  dvdsmultr2  13685  bitsmod  13749  sadadd  13780  sadass  13784  smuval2  13795  smumul  13806  pcmpt  14071  pcmpt2  14072  prmreclem2  14095  prmreclem5  14098  ramcl  14207  mrcidb2  14674  acsfn  14715  latleeqj1  15351  pgpssslw  16233  subgdmdprd  16652  lssle0  17153  islpir2  17455  islinds3  18387  iscld4  18800  discld  18824  cncnpi  19013  cnprest2  19025  lmss  19033  iscon2  19149  dfcon2  19154  subislly  19216  lly1stc  19231  elptr  19277  txcn  19330  hauseqlcld  19350  xkoinjcn  19391  tsmsresOLD  19848  tsmsres  19849  isxmet2d  20033  xmetgt0  20064  prdsxmetlem  20074  imasdsf1olem  20079  xblss2  20108  stdbdbl  20223  prdsxmslem2  20235  xrtgioo  20514  xrsxmet  20517  cncffvrn  20605  cnmpt2pc  20631  elpi1i  20749  minveclem7  21053  elovolmr  21090  ismbf  21240  mbfmax  21259  itg1val2  21294  mbfi1fseqlem4  21328  itgresr  21388  iblrelem  21400  iblpos  21402  itgfsum  21436  rlimcnp  22491  rlimcnp2  22492  chpchtsum  22690  dchreq  22729  lgsneg  22790  lgsdilem  22793  lgsquadlem2  22826  isusgra0  23426  dfconngra1  23708  eupath2lem2  23750  minvecolem7  24435  shle0  24996  mdsl2bi  25878  dmdbr5ati  25977  cdj3lem1  25989  eulerpartlemr  26900  subfacp1lem3  27213  dfres3  27712  hfext  28364  mblfinlem3  28577  mblfinlem4  28578  mbfresfi  28585  itg2addnclem  28590  itg2addnc  28593  cover2  28754  heiborlem10  28866  mrefg3  29191  acsfn1p  29703  funressnfv  30181  dfdfat2  30184  2ffzoeq  30361  frgra3vlem2  30740  numclwwlk2lem1  30842  bj-issetwt  32687  ople0  33155  atlle0  33273  cdlemg10c  34606  cdlemg33c  34675  hdmap14lem13  35851
  Copyright terms: Public domain W3C validator