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

Theorem simprbda 650
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 499 . 2 ((𝜑𝜓) → (𝜒𝜃))
32simpld 473 1 ((𝜑𝜓) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382
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 195  df-an 384
This theorem is referenced by:  elrabi  3327  oteqex  4883  fsnex  6416  fisupg  8071  fiinfg  8266  cantnff  8432  fseqenlem2  8709  fpwwe2lem11  9319  fpwwe2lem12  9320  fpwwe2  9322  rlimsqzlem  14176  ramub1lem2  15518  mriss  16067  invfun  16196  pltle  16733  subgslw  17803  frgpnabllem2  18049  cyggeninv  18057  ablfaclem3  18258  lmodfopnelem1  18671  psrbagf  19135  mplind  19272  pjff  19823  pjf2  19825  pjfo  19826  pjcss  19827  fvmptnn04ifc  20424  chfacfisf  20426  chfacfisfcpmat  20427  tg1  20527  cldss  20591  cnf2  20811  cncnp  20842  lly1stc  21057  refbas  21071  qtoptop2  21260  qtoprest  21278  elfm3  21512  flfelbas  21556  cnextf  21628  restutopopn  21800  cfilufbas  21851  fmucnd  21854  blgt0  21962  xblss2ps  21964  xblss2  21965  tngngp  22216  cfilfil  22818  iscau2  22828  caufpm  22833  cmetcaulem  22839  dvcnp2  23434  dvfsumrlim  23543  dvfsumrlim2  23544  fta1g  23676  dvdsflsumcom  24659  fsumvma  24683  vmadivsumb  24917  dchrisumlema  24922  dchrvmasumlem1  24929  dchrvmasum2lem  24930  dchrvmasumiflem1  24935  selbergb  24983  selberg2b  24986  pntibndlem3  25026  pntlem3  25043  motgrp  25184  oppnid  25384  clwlkiswlk  26079  sspnv  26797  lnof  26828  bloln  26857  reff  29068  signsply0  29788  cvmliftmolem1  30351  cvmlift2lem9a  30373  mbfresfi  32450  itg2gt0cn  32459  ismtyres  32601  ghomf  32683  rngoisohom  32773  pridlidl  32828  pridlnr  32829  maxidlidl  32834  lflf  33192  lkrcl  33221  cvrlt  33399  cvrle  33407  atbase  33418  llnbase  33637  lplnbase  33662  lvolbase  33706  psubssat  33882  lhpbase  34126  laut1o  34213  ldillaut  34239  ltrnldil  34250  diadmclN  35168  pell1234qrre  36258  lnmlsslnm  36493  cvgdvgrat  37358  stoweidlem34  38751
  Copyright terms: Public domain W3C validator