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  3916  posn  5067  elrnmpt1  5249  fliftf  6199  eroveu  7403  ixpfi2  7814  funsnfsupp  7849  elfi2  7870  dffi3  7887  cantnfrescl  8091  cfss  8641  wunex2  9112  nn2ge  10557  nnle1eq1  10560  nn0le0eq0  10820  nn0lt10b  10920  ixxun  11541  ioopos  11597  injresinj  11890  cnpart  13032  fz1f1o  13491  nndivdvds  13849  dvdsmultr2  13876  bitsmod  13941  sadadd  13972  sadass  13976  smuval2  13987  smumul  13998  pcmpt  14266  pcmpt2  14267  prmreclem2  14290  prmreclem5  14293  ramcl  14402  mrcidb2  14869  acsfn  14910  latleeqj1  15546  pgpssslw  16430  subgdmdprd  16871  lssle0  17379  islpir2  17681  islinds3  18636  iscld4  19332  discld  19356  cncnpi  19545  cnprest2  19557  lmss  19565  iscon2  19681  dfcon2  19686  subislly  19748  lly1stc  19763  elptr  19809  txcn  19862  hauseqlcld  19882  xkoinjcn  19923  tsmsresOLD  20380  tsmsres  20381  isxmet2d  20565  xmetgt0  20596  prdsxmetlem  20606  imasdsf1olem  20611  xblss2  20640  stdbdbl  20755  prdsxmslem2  20767  xrtgioo  21046  xrsxmet  21049  cncffvrn  21137  cnmpt2pc  21163  elpi1i  21281  minveclem7  21585  elovolmr  21622  ismbf  21772  mbfmax  21791  itg1val2  21826  mbfi1fseqlem4  21860  itgresr  21920  iblrelem  21932  iblpos  21934  itgfsum  21968  rlimcnp  23023  rlimcnp2  23024  chpchtsum  23222  dchreq  23261  lgsneg  23322  lgsdilem  23325  lgsquadlem2  23358  lmiinv  23835  isusgra0  24023  usgraop  24026  dfconngra1  24347  eupath2lem2  24654  frgra3vlem2  24677  numclwwlk2lem1  24779  minvecolem7  25475  shle0  26036  mdsl2bi  26918  dmdbr5ati  27017  cdj3lem1  27029  eulerpartlemr  27953  subfacp1lem3  28266  dfres3  28765  hfext  29417  mblfinlem3  29630  mblfinlem4  29631  mbfresfi  29638  itg2addnclem  29643  itg2addnc  29646  cover2  29807  heiborlem10  29919  mrefg3  30244  acsfn1p  30753  funressnfv  31680  dfdfat2  31683  2ffzoeq  31810  bj-issetwt  33516  ople0  33984  atlle0  34102  cdlemg10c  35435  cdlemg33c  35504  hdmap14lem13  36680  xpcogend  36783
  Copyright terms: Public domain W3C validator