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

Theorem simplbda 607
Description: Deduction eliminating a conjunct. (Contributed by NM, 22-Oct-2007.)
Hypothesis
Ref Expression
pm3.26bda.1  |-  ( ph  ->  ( ps  <->  ( ch  /\ 
th ) ) )
Assertion
Ref Expression
simplbda  |-  ( (
ph  /\  ps )  ->  th )

Proof of Theorem simplbda
StepHypRef Expression
1 pm3.26bda.1 . . 3  |-  ( ph  ->  ( ps  <->  ( ch  /\ 
th ) ) )
21biimpa 470 . 2  |-  ( (
ph  /\  ps )  ->  ( ch  /\  th ) )
32simprd 449 1  |-  ( (
ph  /\  ps )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358
This theorem is referenced by:  cantnflem3  7393  mapfien  7399  fseqenlem2  7652  axdc3lem2  8077  fpwwe2lem12  8263  rlimsqzlem  12122  ramub1lem2  13074  invfun  13666  pltne  14096  cntzi  14805  odmulg  14869  subgslw  14927  frgpnabllem1  15161  cyggeninv  15170  ablfaclem3  15322  lsslmod  15717  pjff  16612  pjf2  16614  pjcss  16616  ocvpj  16617  tgcl  16707  cldopn  16768  cncnp  17009  1stcelcls  17187  lly1stc  17222  qtoptop2  17390  qtopid  17396  trfg  17586  flfneii  17687  fclsbas  17716  isfcf  17729  blgt0  17956  xblss2  17958  mopni  18038  metrest  18070  cfilss  18696  caun0  18707  cmetcaulem  18714  cfilresi  18721  cnlimci  19239  dvcl  19249  dvcnp  19268  dvcnp2  19269  dvnadd  19278  dvfsumrlimge0  19377  dvfsumrlim  19378  dvfsumrlim2  19379  evlslem3  19398  fta1g  19553  plyeq0lem  19592  vieta1lem1  19690  vieta1lem2  19691  fsumharmonic  20305  dvdsflf1o  20427  dvdsflsumcom  20428  fsumvma  20452  vmadivsumb  20632  dchrisum0lem1a  20635  dchrisumlema  20637  dchrisumlem3  20640  dchrmusum2  20643  dchrvmasumlem2  20647  dchrvmasumiflem1  20650  dchrisum0fno1  20660  dchrisum0lem1b  20664  mulog2sumlem2  20684  vmalogdivsum2  20687  2vmadivsumlem  20689  selberglem2  20695  selbergb  20698  selberg2b  20701  selberg3lem1  20706  selberg4lem1  20709  pntpbnd1  20735  pntibndlem3  20741  pntlem3  20758  sspba  21303  sspg  21304  ssps  21306  sspn  21312  nmblore  21364  phpar  21402  ocorth  21870  elnlfn2  22509  cvmliftmolem1  23812  vidfunid  25837  iddvvidd  25838  idcvvidc  25839  fmp  25840  refssex  26281  fnetr  26286  sstotbnd2  26498  rngoiso1o  26610  pridl  26662  lfli  29251  lkrf0  29283  cvrne  29471  atcvr0  29478  psubspi  29936  psubcli2N  30128  lhp1cvr  30188  lautle  30273  diadmleN  31228
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator