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

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

Proof of Theorem simprbda
StepHypRef Expression
1 pm3.26bda.1 . . 3 (𝜑 → (𝜓 ↔ (𝜒𝜃)))
21biimpa 477 . 2 ((𝜑𝜓) → (𝜒𝜃))
32simpld 495 1 ((𝜑𝜓) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396
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 208  df-an 397
This theorem is referenced by:  elrabi  3679  oteqex  5387  fsnex  7035  fisupg  8760  fiinfg  8957  cantnff  9131  fseqenlem2  9445  fpwwe2lem11  10056  fpwwe2lem12  10057  fpwwe2  10059  rlimsqzlem  15000  ramub1lem2  16358  mriss  16901  invfun  17029  pltle  17566  subgslw  18677  frgpnabllem2  18930  cyggeninv  18938  ablfaclem3  19145  lmodfopnelem1  19606  psrbagf  20080  mplind  20217  mhpmpl  20270  pjff  20791  pjf2  20793  pjfo  20794  pjcss  20795  fvmptnn04ifc  21395  chfacfisf  21397  chfacfisfcpmat  21398  tg1  21507  cldss  21572  cnf2  21792  cncnp  21823  lly1stc  22039  refbas  22053  qtoptop2  22242  qtoprest  22260  elfm3  22493  flfelbas  22537  cnextf  22609  restutopopn  22781  cfilufbas  22832  fmucnd  22835  blgt0  22943  xblss2ps  22945  xblss2  22946  tngngp  23197  cfilfil  23804  iscau2  23814  caufpm  23819  cmetcaulem  23825  dvcnp2  24451  dvfsumrlim  24562  dvfsumrlim2  24563  fta1g  24695  dvdsflsumcom  25698  fsumvma  25722  vmadivsumb  25992  dchrisumlema  25997  dchrvmasumlem1  26004  dchrvmasum2lem  26005  dchrvmasumiflem1  26010  selbergb  26058  selberg2b  26061  pntibndlem3  26101  pntlem3  26118  motgrp  26262  oppnid  26465  sspnv  28436  lnof  28465  bloln  28494  fldexttr  30953  reff  31008  signsply0  31726  cvmliftmolem1  32431  cvmlift2lem9a  32453  mbfresfi  34824  itg2gt0cn  34833  ismtyres  34973  ghomf  35055  rngoisohom  35145  pridlidl  35200  pridlnr  35201  maxidlidl  35206  lflf  36085  lkrcl  36114  cvrlt  36292  cvrle  36300  atbase  36311  llnbase  36531  lplnbase  36556  lvolbase  36600  psubssat  36776  lhpbase  37020  laut1o  37107  ldillaut  37133  ltrnldil  37144  diadmclN  38059  pell1234qrre  39333  lnmlsslnm  39565  cvgdvgrat  40529  stoweidlem34  42204
  Copyright terms: Public domain W3C validator