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

Theorem simplbda 653
Description: Deduction eliminating a conjunct. (Contributed by NM, 22-Oct-2007.)
Hypothesis
Ref Expression
pm3.26bda.1 (𝜑 → (𝜓 ↔ (𝜒𝜃)))
Assertion
Ref Expression
simplbda ((𝜑𝜓) → 𝜃)

Proof of Theorem simplbda
StepHypRef Expression
1 pm3.26bda.1 . . 3 (𝜑 → (𝜓 ↔ (𝜒𝜃)))
21biimpa 500 . 2 ((𝜑𝜓) → (𝜒𝜃))
32simprd 478 1 ((𝜑𝜓) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383
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 197  df-an 385
This theorem is referenced by:  cantnflem3  8626  fseqenlem2  8886  axdc3lem2  9311  fpwwe2lem12  9501  rlimsqzlem  14423  ramub1lem2  15778  invfun  16471  pltne  17009  cntzi  17808  odmulg  18019  subgslw  18077  frgpnabllem1  18322  cyggeninv  18331  ablfaclem3  18532  lsslmod  19008  evlslem3  19562  psgnevpm  19983  pjff  20104  pjf2  20106  pjcss  20108  ocvpj  20109  scmatscmid  20360  fvmptnn04ifc  20705  fvmptnn04ifd  20706  tgcl  20821  cldopn  20883  cncnp  21132  1stcelcls  21312  lly1stc  21347  refssex  21362  qtoptop2  21550  qtopid  21556  trfg  21742  flfneii  21843  fclsbas  21872  isfcf  21885  restutop  22088  restutopopn  22089  isucn2  22130  cfiluexsm  22141  cfilufg  22144  blgt0  22251  xblss2ps  22253  xblss2  22254  mopni  22344  metrest  22376  metustbl  22418  restmetu  22422  cfilss  23114  caun0  23125  cmetcaulem  23132  cfilresi  23139  cmetcusp  23196  cnlimci  23698  dvcl  23708  dvcnp  23727  dvcnp2  23728  dvnadd  23737  dvfsumrlimge0  23838  dvfsumrlim  23839  dvfsumrlim2  23840  fta1g  23972  plyeq0lem  24011  vieta1lem1  24110  vieta1lem2  24111  fsumharmonic  24783  dvdsflf1o  24958  dvdsflsumcom  24959  fsumvma  24983  vmadivsumb  25217  dchrisum0lem1a  25220  dchrisumlema  25222  dchrisumlem3  25225  dchrmusum2  25228  dchrvmasumlem2  25232  dchrvmasumiflem1  25235  dchrisum0fno1  25245  dchrisum0lem1b  25249  mulog2sumlem2  25269  vmalogdivsum2  25272  2vmadivsumlem  25274  selberglem2  25280  selbergb  25283  selberg2b  25286  selberg3lem1  25291  selberg4lem1  25294  pntpbnd1  25320  pntibndlem3  25326  pntlem3  25343  oppnid  25683  sspba  27710  sspg  27711  ssps  27713  sspn  27719  nmblore  27769  phpar  27807  ocorth  28278  elnlfn2  28916  foresf1o  29469  fpwrelmap  29636  kerunit  29951  reff  30034  cnre2csqlem  30084  fmcncfil  30105  elzrhunit  30151  qqhval2lem  30153  baselsiga  30306  signsply0  30756  cvmliftmolem1  31389  mclsppslem  31606  mclspps  31607  fnetr  32471  relowlssretop  33341  mbfresfi  33586  itg2addnclem  33591  itg2addnclem2  33592  sstotbnd2  33703  rngoiso1o  33908  pridl  33966  lfli  34666  lkrf0  34698  cvrne  34886  atcvr0  34893  psubspi  35351  psubcli2N  35543  lhp1cvr  35603  lautle  35688  diadmleN  36644  cvgdvgrat  38829  radcnvrat  38830  islptre  40169  islpcn  40189  icccncfext  40418  fdivmptf  42660  refdivmptf  42661  rege1logbrege0  42677
  Copyright terms: Public domain W3C validator