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

Theorem simpl3 1208
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 474 . 2 ((𝜒𝜃) → 𝜒)
213ad2antl3 1179 1 (((𝜑𝜓𝜒) ∧ 𝜃) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1072
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  df-3an 1074
This theorem is referenced by:  simpll3OLD  1236  simprl3OLD  1248  simpl13  1295  simpl23  1301  simpl33  1307  simp1l3  1329  simp2l3  1335  simp3l3  1341  3anandirs  1572  f1prex  6690  fcofo  6694  soisores  6728  weniso  6755  knatar  6758  ofmpteq  7069  smorndom  7622  nnmord  7869  nnmword  7870  difsnen  8195  mapunen  8282  ac6sfi  8357  fipreima  8425  wemaplem2  8605  wemapso2lem  8610  en2eqpr  8991  indcardi  9025  acndom  9035  fodomfi2  9044  infmap2  9203  cflim2  9248  coftr  9258  infpssrlem4  9291  fin23lem11  9302  fincssdom  9308  isf32lem9  9346  fin1a2lem9  9393  gchpwdom  9655  gruima  9787  prpssnq  9975  distrlem4pr  10011  dedekind  10363  addcan  10383  addcan2  10384  divmulass  10871  supmul1  11155  uzsupss  11944  xaddass  12243  xleadd1a  12247  xlesubadd  12257  xmulasslem3  12280  xmulass  12281  xadddilem  12288  xadddi  12289  ixxun  12355  icoshftf1o  12459  snunioc  12464  difelfzle  12617  fzo1fzo0n0  12684  ssfzoulel  12727  modmuladd  12877  modifeq2int  12897  modaddmulmod  12902  modsubdir  12904  ltexp2a  13077  leexp2  13080  ltexp2r  13082  exple1  13085  expnlbnd2  13160  mulsubdivbinom2  13211  hashtpg  13430  ccatass  13531  ccatopth  13641  swrdccatin12lem2a  13656  swrdccat3  13663  cshinj  13728  s2f1o  13832  limsupgre  14382  addcn2  14494  mulcn2  14496  binomrisefac  14943  bpolydif  14956  dvdsmodexp  15161  modmulconst  15186  dvdsmod  15223  sadass  15366  gcdass  15437  rplpwr  15449  rppwr  15450  rpmulgcd2  15543  rpdvds  15547  rpexp  15605  prmdiveq  15664  hashgcdlem  15666  coprimeprodsq  15686  coprimeprodsq2  15687  pythagtriplem3  15696  pcdvdsb  15746  pcgcd1  15754  dvdsprmpweq  15761  pcbc  15777  0ram  15897  ramz2  15901  ramub1lem1  15903  setsstructOLD  16072  mremre  16437  mrieqv2d  16472  lubun  17295  isnsgrp  17460  issubmnd  17490  gsumccat  17550  frmdss2  17572  sgrp2rid2ex  17586  mulgnn0p1  17724  mulgnnsubcl  17725  mulgneg  17732  mulgdirlem  17744  nmzsubg  17807  ghmmulg  17844  pmtrfv  18043  pmtrmvd  18047  pmtrfb  18056  odmodnn0  18130  oddvdsnn0  18134  odnncl  18135  odmod  18136  oddvds  18137  odeq  18140  odmulgid  18142  odmulg  18144  odmulgeq  18145  odbezout  18146  odf1o1  18158  odf1o2  18159  odngen  18163  odcau  18190  pgpssslw  18200  fislw  18211  lsmless1x  18230  lsmless2x  18231  lsmsubm  18239  lsmmod  18259  lsmmod2  18260  efgsfo  18323  cntzcmn  18416  odadd1  18422  odadd2  18423  odadd  18424  lsmcomx  18430  prdscmnd  18435  gsumconst  18505  ring1eq0  18761  cntzsubr  18985  isabvd  18993  rmodislmod  19104  lspss  19157  0lmhm  19213  reslmhm2  19226  pwssplit0  19231  pwssplit1  19232  lbspss  19255  lspfixed  19301  lsmcv  19314  lspsnat  19318  issubassa  19497  aspss  19505  coe1subfv  19809  coe1tm  19816  xrsdsreclblem  19965  obselocv  20245  frlmsplit2  20285  frlmsslss2  20287  frlmup4  20313  lindff1  20332  lsslindf  20342  lsslinds  20343  islindf4  20350  mpt2matmul  20425  mamutpos  20437  submaval  20560  mdetdiag  20578  mdetunilem1  20591  mdetunilem3  20593  mdetunilem9  20599  mdetmul  20602  maducoeval2  20619  madurid  20623  minmar1val  20627  cramer  20670  cpmatel2  20691  m2cpm  20719  decpmatmul  20750  pmatcollpw1lem2  20753  pmatcollpw1  20754  pmatcollpw2lem  20755  pm2mpcl  20775  mply1topmatcl  20783  mp2pm2mplem2  20785  mp2pm2mplem4  20787  pm2mpghmlem2  20790  pm2mpghmlem1  20791  cayhamlem2  20862  neiint  21081  topssnei  21101  cnrest2  21263  cnprest2  21267  cnt0  21323  cnt1  21327  cnhaus  21331  cncmp  21368  fiuncmp  21380  sscmp  21381  hauscmp  21383  cnconn  21398  unconn  21405  comppfsc  21508  kgen2ss  21531  ptpjopn  21588  ptrescn  21615  qtopss  21691  kqfvima  21706  r0cld  21714  cmphaushmeo  21776  fbssint  21814  fbasrn  21860  filuni  21861  ufilmax  21883  fin1aufil  21908  fmf  21921  fmss  21922  rnelfmlem  21928  rnelfm  21929  fmufil  21935  fmco  21937  flimss2  21948  flimss1  21949  flimrest  21959  cnpflf2  21976  cnpflf  21977  flfcnp  21980  lmflf  21981  supnfcls  21996  fclsss1  21998  fclsss2  21999  cnpfcfi  22016  subgntr  22082  opnsubg  22083  cldsubg  22086  ustuqtop1  22217  ucncn  22261  bldisj  22375  blgt0  22376  bl2in  22377  blss2ps  22380  blss2  22381  xbln0  22391  blssps  22401  blss  22402  lpbl  22480  blcld  22482  blcls  22483  stdbdmopn  22495  metcnp2  22519  txmetcnp  22524  blval2  22539  restmetu  22547  nmoix  22705  nmoi2  22706  nmoeq0  22712  nmotri  22715  metdsge  22824  metds0  22825  metdseq0  22829  icoopnst  22910  iccpnfhmeo  22916  xrhmeo  22917  nmhmcn  23091  cphsqrtcl2  23157  cphsqrtcl3  23158  fmcfil  23241  bcthlem5  23296  cmetcusp1  23320  pjth  23381  ovolunnul  23439  volun  23484  voliunlem2  23490  itg2const  23677  iblconst  23754  itgconst  23755  limcvallem  23805  dvcnp2  23853  dvcn  23854  deg1mul3le  24046  deg1tmle  24047  ig1pdvds  24106  coe11  24179  dgrmulc  24197  dvply1  24209  aaliou2  24265  efcvx  24373  tanord  24454  logdivlti  24536  logccv  24579  recxpcl  24591  cxplea  24612  cxple2a  24615  ang180  24714  isosctrlem2  24719  cxp2lim  24873  amgm  24887  muval1  25029  dvdssqf  25034  mumullem2  25076  bcmono  25172  lgsneg  25216  lgsmod  25218  lgsdirprm  25226  lgsdir  25227  lgsdi  25229  brbtwn2  25955  colinearalglem1  25956  colinearalg  25960  axcgrtr  25965  axcontlem2  26015  upgrewlkle2  26683  wlksoneq1eq2  26741  crctcshwlkn0lem5  26888  wspthsnwspthsnon  27005  wspthsnwspthsnonOLD  27007  lppthon  27274  upgriseupth  27330  4cyclusnfrgr  27417  numclwlk1lem2foa  27484  numclwwlk5  27527  nvmul0or  27785  shless  28498  shlej1  28499  pjspansn  28716  kbmul  29094  homco2  29116  kbass2  29256  padct  29777  eliccelico  29819  elicoelioo  29820  iocinioc2  29821  difioo  29824  xrge0npcan  29974  isarchi2  30019  archiabl  30032  mdetlap1  30172  pstmfval  30219  fmcncfil  30257  zrhnm  30293  qqhnm  30314  nexple  30351  volfiniune  30573  omsmeas  30665  eulerpartlemb  30710  probinc  30763  cndprob01  30777  signswmnd  30914  cvmsss2  31534  dvdspw  31914  funsseq  31944  frpomin  32015  sltres  32092  nolt02olem  32121  nolt02o  32122  nosupbnd1lem1  32131  nosupbnd1lem4  32134  nosupbnd1lem5  32135  nosupbnd1lem6  32136  cgrtriv  32386  5segofs  32390  btwntriv2  32396  btwnxfr  32440  segcon2  32489  brsegle2  32493  seglelin  32500  outsideofeu  32515  lindsenlbs  33686  mblfinlem2  33729  blbnd  33868  rrndstprj2  33912  zerdivemp1x  34028  lsmsat  34767  lsatfixedN  34768  lssat  34775  lkrlsp  34861  lshpkrlem4  34872  cvrcon3b  35036  leat3  35054  atlen0  35069  atnle  35076  atlatmstc  35078  atlatle  35079  cvlcvr1  35098  cvlsupr2  35102  hlsupr2  35145  hlrelat2  35161  cvrexchlem  35177  cvratlem  35179  lnnat  35185  atexchcvrN  35198  1cvratlt  35232  1cvrjat  35233  3atlem3  35243  3atlem7  35247  llni2  35270  atcvrlln2  35277  llnexatN  35279  llncmp  35280  2llnmat  35282  2at0mat0  35283  2atnelpln  35302  llncvrlpln2  35315  2lplnmN  35317  2llnmj  35318  lplncmp  35320  lplnexatN  35321  2llnjaN  35324  lvoli3  35335  islvol2aN  35350  4atlem3a  35355  4atlem4a  35357  4atlem4b  35358  4atlem11  35367  4atlem12  35370  lplncvrlvol2  35373  lvolcmp  35375  2lplnmj  35380  islinei  35498  linepmap  35533  lneq2at  35536  2llnma3r  35546  elpaddn0  35558  elpaddatriN  35561  elpaddat  35562  paddcom  35571  paddss1  35575  paddss2  35576  paddasslem6  35583  paddasslem7  35584  paddasslem10  35587  paddasslem15  35592  pmodlem2  35605  pmodl42N  35609  pmapjoin  35610  atmod1i1m  35616  llnmod1i2  35618  llnexchb2lem  35626  polcon2bN  35678  pclfinclN  35708  poml4N  35711  poml6N  35713  osumcllem11N  35724  osumclN  35725  pmapojoinN  35726  pexmidlem2N  35729  pexmidlem3N  35730  pexmidlem4N  35731  pexmidlem6N  35733  pexmidlem7N  35734  pl42lem2N  35738  pl42lem3N  35739  pl42lem4N  35740  pl42N  35741  lhpexle3lem  35769  lhpmcvr3  35783  lhp2at0nle  35793  lhprelat3N  35798  lauteq  35853  lautco  35855  ltrncoidN  35886  ltrneq2  35906  ltrnnidn  35933  ltrnideq  35934  trlnle  35945  cdlemc  35956  cdlemd4  35960  cdlemd5  35961  cdlemd9  35965  cdlemd  35966  ltrneq3  35967  cdlemefrs29pre00  36154  cdlemefrs29cpre1  36157  cdlemefrs29clN  36158  cdlemefrs32fva  36159  cdlemefr29exN  36161  cdlemefr27cl  36162  cdlemefs27cl  36172  cdlemefs32sn1aw  36173  cdleme32fva  36196  cdleme32d  36203  cdleme32f  36205  cdleme32le  36206  cdleme40n  36227  cdleme41snaw  36235  cdleme17d3  36255  cdleme48fvg  36259  cdlemeg46fvcl  36265  cdlemeg46fgN  36293  cdleme48fgv  36297  ltrniotavalbN  36343  cdlemb3  36365  cdlemg15  36415  cdlemg17dN  36422  trlco  36486  cdlemg44b  36491  ltrncom  36497  trljco  36499  tendococl  36531  tendoplcl  36540  tendoplcom  36541  tendotr  36589  cdlemk36  36672  cdlemk35s-id  36697  cdlemk39s-id  36699  cdlemk19x  36702  cdlemk53b  36715  cdlemk55  36720  cdlemk35u  36723  cdlemk55u  36725  cdlemk39u  36727  cdlemk19u  36729  cdlemk56  36730  tendoex  36734  cdleml5N  36739  dihord2pre  36985  dihord6apre  37016  dihord5b  37019  dihord5apre  37022  dihord  37024  dihmeetlem1N  37050  dihmeetlem2N  37059  dihglbcpreN  37060  dihmeetbN  37063  dihmeetlem4preN  37066  dihmeetlem5  37068  dihmeetlem6  37069  dihmeetlem7N  37070  dihmeetlem10N  37076  dihmeetlem11N  37077  dihmeetlem12N  37078  dihmeetlem13N  37079  dihmeetlem15N  37081  dihmeetlem17N  37083  dihmeetlem18N  37084  dihmeetlem19N  37085  dihmeetALTN  37087  dih1dimatlem0  37088  dihlspsnssN  37092  dvh3dim2  37208  mzpsubst  37782  diophrw  37793  eldioph2lem1  37794  rencldnfi  37856  pellexlem2  37865  pellqrexplicit  37912  infmrgelbi  37913  rmxycomplete  37953  congadd  38004  acongeq  38021  jm2.19  38031  jm2.22  38033  jm2.20nn  38035  jm2.25lem1  38036  jm2.27  38046  jm3.1  38058  lmhmlnmsplit  38128  pwssplit4  38130  hbtlem2  38165  dgraa0p  38190  idomrootle  38244  proot1hash  38249  iocunico  38267  relexpxpmin  38480  brtrclfv2  38490  ntrclsk3  38839  suprnmpt  39823  wessf1ornlem  39839  choicefi  39860  supxrgere  40016  supxrgelem  40020  supxrge  40021  infleinflem2  40054  snunioo1  40210  iccintsng  40221  fmul01  40284  lptre2pt  40344  0ellimcdiv  40353  fnlimfvre  40378  limsupmnfuzlem  40430  climisp  40450  limsupgtlem  40481  ibliccsinexp  40638  iblioosinexp  40640  volioc  40660  iblspltprt  40661  stoweidlem20  40709  stoweidlem22  40711  stoweidlem34  40723  stoweidlem44  40733  stoweidlem60  40749  wallispilem3  40756  fourierdlem42  40838  fourierdlem51  40846  fourierdlem54  40849  fourierdlem87  40882  fourierdlem97  40892  ioorrnopnlem  40996  sge0seq  41135  hoicvr  41237  ccatpfx  41888  pfxccat3  41905  lincresunit3lem3  42742  lindssnlvec  42754
  Copyright terms: Public domain W3C validator