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

Theorem biantrud 495
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 491 . 2  |-  ( ps 
->  ( ch  <->  ( ch  /\ 
ps ) ) )
31, 2syl 16 1  |-  ( ph  ->  ( ch  <->  ( ch  /\ 
ps ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    /\ wa 360
This theorem is referenced by:  posn  4949  elrnmpt1  5122  fliftf  6040  eroveu  7002  ixpfi2  7408  elfi2  7422  dffi3  7439  cantnfrescl  7635  cfss  8150  wunex2  8618  nn2ge  10030  nnle1eq1  10033  nn0le0eq0  10255  nn0lt10b  10341  ixxun  10937  ioopos  10992  injresinj  11205  cnpart  12050  fz1f1o  12509  nndivdvds  12863  dvdsmultr2  12890  bitsmod  12953  sadadd  12984  sadass  12988  smuval2  12999  smumul  13010  pcmpt  13266  pcmpt2  13267  prmreclem2  13290  prmreclem5  13293  ramcl  13402  mrcidb2  13848  acsfn  13889  latleeqj1  14497  pgpssslw  15253  subgdmdprd  15597  lssle0  16031  islpir2  16327  iscld4  17134  discld  17158  cncnpi  17347  cnprest2  17359  lmss  17367  iscon2  17482  dfcon2  17487  subislly  17549  lly1stc  17564  elptr  17610  txcn  17663  hauseqlcld  17683  xkoinjcn  17724  tsmsres  18178  isxmet2d  18362  xmetgt0  18393  prdsxmetlem  18403  imasdsf1olem  18408  xblss2  18437  stdbdbl  18552  prdsxmslem2  18564  xrtgioo  18842  xrsxmet  18845  cncffvrn  18933  cnmpt2pc  18958  elpi1i  19076  minveclem7  19341  elovolmr  19377  ismbf  19525  mbfmax  19544  itg1val2  19579  mbfi1fseqlem4  19613  itgresr  19673  iblrelem  19685  iblpos  19687  itgfsum  19721  rlimcnp  20809  rlimcnp2  20810  chpchtsum  21008  dchreq  21047  lgsneg  21108  lgsdilem  21111  lgsquadlem2  21144  isusgra0  21381  dfconngra1  21663  eupath2lem2  21705  minvecolem7  22390  shle0  22949  mdsl2bi  23831  dmdbr5ati  23930  cdj3lem1  23942  subfacp1lem3  24873  dfres3  25387  hfext  26129  wl-sbrim  26242  mblfinlem3  26257  mblfinlem4  26258  mbfresfi  26265  itg2addnclem  26270  itg2addnc  26273  cover2  26429  heiborlem10  26543  mrefg3  26776  islinds3  27295  acsfn1p  27498  funressnfv  27982  dfdfat2  27985  2ffzoeq  28163  frgra3vlem2  28465  ople0  30059  atlle0  30177  cdlemg10c  31510  cdlemg33c  31579  hdmap14lem13  32755
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 179  df-an 362
  Copyright terms: Public domain W3C validator