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

Theorem simpl3 1239
Description: Simplification of conjunction. (Contributed by Jeff Hankins, 17-Nov-2009.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)
Assertion
Ref Expression
simpl3 (((𝜑𝜓𝜒) ∧ 𝜃) → 𝜒)

Proof of Theorem simpl3
StepHypRef Expression
1 simpl 470 . 2 ((𝜒𝜃) → 𝜒)
213ad2antl3 1231 1 (((𝜑𝜓𝜒) ∧ 𝜃) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1100
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 198  df-an 385  df-3an 1102
This theorem is referenced by:  simpll3OLD  1267  simprl3OLD  1279  simpl13  1326  simpl23  1332  simpl33  1338  simp1l3  1360  simp2l3  1366  simp3l3  1372  3anandirs  1589  f1prex  6761  fcofo  6765  soisores  6799  weniso  6826  knatar  6829  ofmpteq  7144  smorndom  7699  nnmord  7947  nnmword  7948  difsnen  8279  mapunen  8366  ac6sfi  8441  fipreima  8509  wemaplem2  8689  wemapso2lem  8694  en2eqpr  9111  indcardi  9145  acndom  9155  fodomfi2  9164  infmap2  9323  cflim2  9368  coftr  9378  infpssrlem4  9411  fin23lem11  9422  fincssdom  9428  isf32lem9  9466  fin1a2lem9  9513  gchpwdom  9775  gruima  9907  prpssnq  10095  distrlem4pr  10131  dedekind  10483  addcan  10503  addcan2  10504  divmulass  10991  supmul1  11275  uzsupss  11997  xaddass  12295  xleadd1a  12299  xlesubadd  12309  xmulasslem3  12332  xmulass  12333  xadddilem  12340  xadddi  12341  ixxun  12407  icoshftf1o  12514  snunioc  12521  difelfzle  12674  fzo1fzo0n0  12741  ssfzoulel  12784  modmuladd  12934  modifeq2int  12954  modaddmulmod  12959  modsubdir  12961  ltexp2a  13133  leexp2  13136  ltexp2r  13138  exple1  13141  expnlbnd2  13216  mulsubdivbinom2  13267  hashtpg  13482  ccatass  13583  ccatopth  13692  swrdccatin12lem2a  13707  swrdccat3  13714  cshinj  13779  s2f1o  13883  limsupgre  14433  addcn2  14545  mulcn2  14547  binomrisefac  14991  bpolydif  15004  dvdsmodexp  15209  modmulconst  15234  dvdsmod  15271  sadass  15410  gcdass  15481  rplpwr  15493  rppwr  15494  rpmulgcd2  15586  rpdvds  15590  rpexp  15647  prmdiveq  15706  hashgcdlem  15708  coprimeprodsq  15728  coprimeprodsq2  15729  pythagtriplem3  15738  pcdvdsb  15788  pcgcd1  15796  dvdsprmpweq  15803  pcbc  15819  0ram  15939  ramz2  15943  ramub1lem1  15945  setsstructOLD  16108  mremre  16467  mrieqv2d  16502  lubun  17326  isnsgrp  17491  issubmnd  17521  gsumccat  17581  frmdss2  17603  sgrp2rid2ex  17617  mulgnn0p1  17755  mulgnnsubcl  17756  mulgneg  17762  mulgdirlem  17773  nmzsubg  17835  ghmmulg  17872  pmtrfv  18071  pmtrmvd  18075  pmtrfb  18084  odmodnn0  18158  oddvdsnn0  18162  odnncl  18163  odmod  18164  oddvds  18165  odeq  18168  odmulgid  18170  odmulg  18172  odmulgeq  18173  odbezout  18174  odf1o1  18186  odf1o2  18187  odngen  18191  odcau  18218  pgpssslw  18228  fislw  18239  lsmless1x  18258  lsmless2x  18259  lsmsubm  18267  lsmmod  18287  lsmmod2  18288  efgsfo  18351  cntzcmn  18444  odadd1  18450  odadd2  18451  odadd  18452  lsmcomx  18458  prdscmnd  18463  gsumconst  18533  ring1eq0  18790  cntzsubr  19014  isabvd  19022  rmodislmod  19133  lspss  19189  0lmhm  19245  reslmhm2  19258  pwssplit0  19263  pwssplit1  19264  lbspss  19287  lspfixed  19333  lspfixedOLD  19334  lsmcv  19347  lspsnat  19351  issubassa  19531  aspss  19539  coe1subfv  19842  coe1tm  19849  xrsdsreclblem  19998  obselocv  20280  frlmsplit2  20320  frlmsslss2  20322  frlmup4  20348  lindff1  20367  lsslindf  20377  lsslinds  20378  islindf4  20385  mpt2matmul  20461  mamutpos  20473  submaval  20596  mdetdiag  20614  mdetunilem1  20627  mdetunilem3  20629  mdetunilem9  20635  mdetmul  20638  maducoeval2  20655  madurid  20659  minmar1val  20663  cramer  20708  cpmatel2  20729  m2cpm  20757  decpmatmul  20788  pmatcollpw1lem2  20791  pmatcollpw1  20792  pmatcollpw2lem  20793  pm2mpcl  20813  mply1topmatcl  20821  mp2pm2mplem2  20823  mp2pm2mplem4  20825  pm2mpghmlem2  20828  pm2mpghmlem1  20829  cayhamlem2  20900  neiint  21120  topssnei  21140  cnrest2  21302  cnprest2  21306  cnt0  21362  cnt1  21366  cnhaus  21370  cncmp  21407  fiuncmp  21419  sscmp  21420  hauscmp  21422  cnconn  21437  unconn  21444  comppfsc  21547  kgen2ss  21570  ptpjopn  21627  ptrescn  21654  qtopss  21730  kqfvima  21745  r0cld  21753  cmphaushmeo  21815  fbssint  21853  fbasrn  21899  filuni  21900  ufilmax  21922  fin1aufil  21947  fmf  21960  fmss  21961  rnelfmlem  21967  rnelfm  21968  fmufil  21974  fmco  21976  flimss2  21987  flimss1  21988  flimrest  21998  cnpflf2  22015  cnpflf  22016  flfcnp  22019  lmflf  22020  supnfcls  22035  fclsss1  22037  fclsss2  22038  cnpfcfi  22055  subgntr  22121  opnsubg  22122  cldsubg  22125  ustuqtop1  22256  ucncn  22300  bldisj  22414  blgt0  22415  bl2in  22416  blss2ps  22419  blss2  22420  xbln0  22430  blssps  22440  blss  22441  lpbl  22519  blcld  22521  blcls  22522  stdbdmopn  22534  metcnp2  22558  txmetcnp  22563  blval2  22578  restmetu  22586  nmoix  22744  nmoi2  22745  nmoeq0  22751  nmotri  22754  metdsge  22863  metds0  22864  metdseq0  22868  icoopnst  22949  iccpnfhmeo  22955  xrhmeo  22956  nmhmcn  23130  cphsqrtcl2  23196  cphsqrtcl3  23197  fmcfil  23280  bcthlem5  23335  cmetcusp1  23359  pjth  23420  ovolunnul  23479  volun  23524  voliunlem2  23530  itg2const  23719  iblconst  23796  itgconst  23797  limcvallem  23847  dvcnp2  23895  dvcn  23896  deg1mul3le  24088  deg1tmle  24089  ig1pdvds  24148  coe11  24221  dgrmulc  24239  dvply1  24251  aaliou2  24307  efcvx  24415  tanord  24497  logdivlti  24578  logccv  24621  recxpcl  24633  cxplea  24654  cxple2a  24657  ang180  24756  isosctrlem2  24761  cxp2lim  24915  amgm  24929  muval1  25071  dvdssqf  25076  mumullem2  25118  bcmono  25214  lgsneg  25258  lgsmod  25260  lgsdirprm  25268  lgsdir  25269  lgsdi  25271  brbtwn2  25997  colinearalglem1  25998  colinearalg  26002  axcgrtr  26007  axcontlem2  26057  upgrewlkle2  26728  wlksoneq1eq2  26786  crctcshwlkn0lem5  26933  wspthsnwspthsnon  27052  wspthsnwspthsnonOLD  27054  lppthon  27322  upgriseupth  27378  4cyclusnfrgr  27465  numclwwlk1lem2foa  27531  numclwwlk5  27574  nvmul0or  27831  shless  28544  shlej1  28545  pjspansn  28762  kbmul  29140  homco2  29162  kbass2  29302  padct  29822  eliccelico  29864  elicoelioo  29865  iocinioc2  29866  difioo  29869  xrge0npcan  30017  isarchi2  30062  archiabl  30075  mdetlap1  30215  pstmfval  30262  fmcncfil  30300  zrhnm  30336  qqhnm  30357  nexple  30394  volfiniune  30616  omsmeas  30708  eulerpartlemb  30753  probinc  30806  cndprob01  30820  signswmnd  30957  cvmsss2  31577  dvdspw  31956  funsseq  31986  frpomin  32057  sltres  32134  nolt02olem  32163  nolt02o  32164  nosupbnd1lem1  32173  nosupbnd1lem4  32176  nosupbnd1lem5  32177  nosupbnd1lem6  32178  cgrtriv  32428  5segofs  32432  btwntriv2  32438  btwnxfr  32482  segcon2  32531  brsegle2  32535  seglelin  32542  outsideofeu  32557  lindsenlbs  33715  mblfinlem2  33758  blbnd  33895  rrndstprj2  33939  zerdivemp1x  34055  lsmsat  34786  lsatfixedN  34787  lssat  34794  lkrlsp  34880  lshpkrlem4  34891  cvrcon3b  35055  leat3  35073  atlen0  35088  atnle  35095  atlatmstc  35097  atlatle  35098  cvlcvr1  35117  cvlsupr2  35121  hlsupr2  35165  hlrelat2  35181  cvrexchlem  35197  cvratlem  35199  lnnat  35205  atexchcvrN  35218  1cvratlt  35252  1cvrjat  35253  3atlem3  35263  3atlem7  35267  llni2  35290  atcvrlln2  35297  llnexatN  35299  llncmp  35300  2llnmat  35302  2at0mat0  35303  2atnelpln  35322  llncvrlpln2  35335  2lplnmN  35337  2llnmj  35338  lplncmp  35340  lplnexatN  35341  2llnjaN  35344  lvoli3  35355  islvol2aN  35370  4atlem3a  35375  4atlem4a  35377  4atlem4b  35378  4atlem11  35387  4atlem12  35390  lplncvrlvol2  35393  lvolcmp  35395  2lplnmj  35400  islinei  35518  linepmap  35553  lneq2at  35556  2llnma3r  35566  elpaddn0  35578  elpaddatriN  35581  elpaddat  35582  paddcom  35591  paddss1  35595  paddss2  35596  paddasslem6  35603  paddasslem7  35604  paddasslem10  35607  paddasslem15  35612  pmodlem2  35625  pmodl42N  35629  pmapjoin  35630  atmod1i1m  35636  llnmod1i2  35638  llnexchb2lem  35646  polcon2bN  35698  pclfinclN  35728  poml4N  35731  poml6N  35733  osumcllem11N  35744  osumclN  35745  pmapojoinN  35746  pexmidlem2N  35749  pexmidlem3N  35750  pexmidlem4N  35751  pexmidlem6N  35753  pexmidlem7N  35754  pl42lem2N  35758  pl42lem3N  35759  pl42lem4N  35760  pl42N  35761  lhpexle3lem  35789  lhpmcvr3  35803  lhp2at0nle  35813  lhprelat3N  35818  lauteq  35873  lautco  35875  ltrncoidN  35906  ltrneq2  35926  ltrnnidn  35953  ltrnideq  35954  trlnle  35965  cdlemc  35976  cdlemd4  35980  cdlemd5  35981  cdlemd9  35985  cdlemd  35986  ltrneq3  35987  cdlemefrs29pre00  36174  cdlemefrs29cpre1  36177  cdlemefrs29clN  36178  cdlemefrs32fva  36179  cdlemefr29exN  36181  cdlemefr27cl  36182  cdlemefs27cl  36192  cdlemefs32sn1aw  36193  cdleme32fva  36216  cdleme32d  36223  cdleme32f  36225  cdleme32le  36226  cdleme40n  36247  cdleme41snaw  36255  cdleme17d3  36275  cdleme48fvg  36279  cdlemeg46fvcl  36285  cdlemeg46fgN  36313  cdleme48fgv  36317  ltrniotavalbN  36363  cdlemb3  36385  cdlemg15  36435  cdlemg17dN  36442  trlco  36506  cdlemg44b  36511  ltrncom  36517  trljco  36519  tendococl  36551  tendoplcl  36560  tendoplcom  36561  tendotr  36609  cdlemk36  36692  cdlemk35s-id  36717  cdlemk39s-id  36719  cdlemk19x  36722  cdlemk53b  36735  cdlemk55  36740  cdlemk35u  36743  cdlemk55u  36745  cdlemk39u  36747  cdlemk19u  36749  cdlemk56  36750  tendoex  36754  cdleml5N  36759  dihord2pre  37004  dihord6apre  37035  dihord5b  37038  dihord5apre  37041  dihord  37043  dihmeetlem1N  37069  dihmeetlem2N  37078  dihglbcpreN  37079  dihmeetbN  37082  dihmeetlem4preN  37085  dihmeetlem5  37087  dihmeetlem6  37088  dihmeetlem7N  37089  dihmeetlem10N  37095  dihmeetlem11N  37096  dihmeetlem12N  37097  dihmeetlem13N  37098  dihmeetlem15N  37100  dihmeetlem17N  37102  dihmeetlem18N  37103  dihmeetlem19N  37104  dihmeetALTN  37106  dih1dimatlem0  37107  dihlspsnssN  37111  dvh3dim2  37227  mzpsubst  37811  diophrw  37822  eldioph2lem1  37823  rencldnfi  37885  pellexlem2  37894  pellqrexplicit  37941  infmrgelbi  37942  rmxycomplete  37981  congadd  38032  acongeq  38049  jm2.19  38059  jm2.22  38061  jm2.20nn  38063  jm2.25lem1  38064  jm2.27  38074  jm3.1  38086  lmhmlnmsplit  38156  pwssplit4  38158  hbtlem2  38193  dgraa0p  38218  idomrootle  38272  proot1hash  38277  iocunico  38294  relexpxpmin  38507  brtrclfv2  38517  ntrclsk3  38866  suprnmpt  39842  wessf1ornlem  39858  choicefi  39877  supxrgere  40027  supxrgelem  40031  supxrge  40032  infleinflem2  40065  snunioo1  40217  iccintsng  40228  fmul01  40290  lptre2pt  40350  0ellimcdiv  40359  fnlimfvre  40384  limsupmnfuzlem  40436  climisp  40456  limsupgtlem  40487  ibliccsinexp  40644  iblioosinexp  40646  volioc  40665  iblspltprt  40666  stoweidlem20  40714  stoweidlem22  40716  stoweidlem34  40728  stoweidlem44  40738  stoweidlem60  40754  wallispilem3  40761  fourierdlem42  40843  fourierdlem51  40851  fourierdlem54  40854  fourierdlem87  40887  fourierdlem97  40897  ioorrnopnlem  41001  sge0seq  41140  hoicvr  41242  ccatpfx  41982  pfxccat3  41999  lincresunit3lem3  42829  lindssnlvec  42841
  Copyright terms: Public domain W3C validator