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

Theorem biantrud 505
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 501 . 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 367
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 369
This theorem is referenced by:  cad1  1468  raldifeq  3905  posn  5057  elrnmpt1  5240  fliftf  6188  eroveu  7398  ixpfi2  7810  funsnfsupp  7845  elfi2  7866  dffi3  7883  cfss  8636  wunex2  9105  nn2ge  10556  nnle1eq1  10559  nn0le0eq0  10820  nn0lt10bOLD  10922  ixxun  11548  ioopos  11604  injresinj  11907  xpcogend  12895  cnpart  13158  fz1f1o  13617  nndivdvds  14079  dvdsmultr2  14108  bitsmod  14173  sadadd  14204  sadass  14208  smuval2  14219  smumul  14230  pcmpt  14498  pcmpt2  14499  prmreclem2  14522  prmreclem5  14525  ramcl  14634  mrcidb2  15110  acsfn  15151  fncnvimaeqv  15591  latleeqj1  15895  pgpssslw  16836  subgdmdprd  17279  lssle0  17794  islpir2  18097  islinds3  19039  iscld4  19736  discld  19760  cncnpi  19949  cnprest2  19961  lmss  19969  iscon2  20084  dfcon2  20089  subislly  20151  lly1stc  20166  elptr  20243  txcn  20296  hauseqlcld  20316  xkoinjcn  20357  tsmsresOLD  20814  tsmsres  20815  isxmet2d  20999  xmetgt0  21030  prdsxmetlem  21040  imasdsf1olem  21045  xblss2  21074  stdbdbl  21189  prdsxmslem2  21201  xrtgioo  21480  xrsxmet  21483  cncffvrn  21571  cnmpt2pc  21597  elpi1i  21715  minveclem7  22019  elovolmr  22056  ismbf  22206  mbfmax  22225  itg1val2  22260  mbfi1fseqlem4  22294  itgresr  22354  iblrelem  22366  iblpos  22368  itgfsum  22402  rlimcnp  23496  rlimcnp2  23497  chpchtsum  23695  dchreq  23734  lgsneg  23795  lgsdilem  23798  lgsquadlem2  23831  lmiinv  24362  isusgra0  24552  usgraop  24555  dfconngra1  24876  eupath2lem2  25183  frgra3vlem2  25206  numclwwlk2lem1  25307  minvecolem7  26000  shle0  26561  mdsl2bi  27443  dmdbr5ati  27542  cdj3lem1  27554  eulerpartlemr  28580  subfacp1lem3  28893  dfres3  29432  hfext  30071  mblfinlem3  30296  mblfinlem4  30297  mbfresfi  30304  itg2addnclem  30309  itg2addnc  30312  cover2  30447  heiborlem10  30559  mrefg3  30883  acsfn1p  31392  radcnvrat  31439  funressnfv  32455  dfdfat2  32458  2ffzoeq  32734  bj-issetwt  34855  ople0  35328  atlle0  35446  cdlemg10c  36781  cdlemg33c  36850  hdmap14lem13  38026
  Copyright terms: Public domain W3C validator