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

Theorem simpl3 1185
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 483 . 2 ((𝜒𝜃) → 𝜒)
213ad2antl3 1179 1 (((𝜑𝜓𝜒) ∧ 𝜃) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1079
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  df-3an 1081
This theorem is referenced by:  simpl13  1242  simpl23  1245  simpl33  1248  simp1l3  1260  simp2l3  1266  simp3l3  1272  3anandirs  1463  2nreu  4391  f1prex  7031  fcofo  7035  soisores  7069  weniso  7096  knatar  7099  ofmpteq  7417  funelss  7737  smorndom  7996  nnmord  8248  nnmword  8249  difsnen  8588  mapunen  8675  ac6sfi  8751  fipreima  8819  wemaplem2  9000  wemapso2lem  9005  en2eqpr  9422  indcardi  9456  acndom  9466  fodomfi2  9475  infmap2  9629  cflim2  9674  coftr  9684  infpssrlem4  9717  fin23lem11  9728  fincssdom  9734  isf32lem9  9772  fin1a2lem9  9819  gchpwdom  10081  gruima  10213  prpssnq  10401  distrlem4pr  10437  dedekind  10792  addcan  10813  addcan2  10814  divmulass  11310  supmul1  11599  uzsupss  12329  xaddass  12632  xleadd1a  12636  xlesubadd  12646  xmulasslem3  12669  xmulass  12670  xadddilem  12677  xadddi  12678  ixxun  12744  icoshftf1o  12850  snunioc  12856  difelfzle  13010  fzo1fzo0n0  13078  ssfzoulel  13121  modmuladd  13271  modifeq2int  13291  modaddmulmod  13296  modsubdir  13298  ltexp2a  13520  leexp2  13525  ltexp2r  13527  exple1  13530  expnlbnd2  13585  mulsubdivbinom2  13612  hashtpg  13833  ccatass  13932  ccatopth  14068  pfxccatin12lem2a  14079  pfxccat3  14086  cshinj  14163  2cshw  14165  s2f1o  14268  limsupgre  14828  addcn2  14940  mulcn2  14942  binomrisefac  15386  bpolydif  15399  dvdsmodexp  15605  modmulconst  15631  dvdsmod  15668  sadass  15810  gcdass  15885  rplpwr  15897  rppwr  15898  rpmulgcd2  15990  rpdvds  15994  rpexp  16054  prmdiveq  16113  hashgcdlem  16115  coprimeprodsq  16135  coprimeprodsq2  16136  pythagtriplem3  16145  pcdvdsb  16195  pcgcd1  16203  dvdsprmpweq  16210  pcbc  16226  0ram  16346  ramz2  16350  ramub1lem1  16352  mremre  16865  mrieqv2d  16900  lubun  17723  isnsgrp  17895  issubmnd  17928  gsumccatOLD  17995  frmdss2  18018  sgrp2rid2ex  18032  mulgnn0p1  18179  mulgnnsubcl  18180  mulgneg  18186  mulgdirlem  18198  nmzsubg  18257  ghmmulg  18310  pmtrfv  18511  pmtrmvd  18515  pmtrfb  18524  odmodnn0  18599  oddvdsnn0  18603  odnncl  18604  odmod  18605  oddvds  18606  odeq  18609  odmulgid  18612  odmulg  18614  odmulgeq  18615  odbezout  18616  odf1o1  18628  odf1o2  18629  odngen  18633  odcau  18660  pgpssslw  18670  fislw  18681  lsmless1x  18700  lsmless2x  18701  lsmsubm  18709  lsmmod  18732  lsmmod2  18733  efgsfo  18796  cntzcmn  18891  odadd1  18899  odadd2  18900  odadd  18901  lsmcomx  18907  prdscmnd  18912  gsumconst  18985  ring1eq0  19271  cntzsubr  19499  isabvd  19522  rmodislmod  19633  lspss  19687  0lmhm  19743  reslmhm2  19756  pwssplit0  19761  pwssplit1  19762  lbspss  19785  lspfixed  19831  lsmcv  19844  lspsnat  19848  issubassa  20028  aspss  20036  coe1subfv  20364  coe1tm  20371  xrsdsreclblem  20521  obselocv  20802  frlmsplit2  20847  frlmsslss2  20849  frlmup4  20875  lindff1  20894  lsslindf  20904  lsslinds  20905  islindf4  20912  mpomatmul  20985  mamutpos  20997  submaval  21120  mdetdiag  21138  mdetunilem1  21151  mdetunilem3  21153  mdetunilem9  21159  mdetmul  21162  maducoeval2  21179  madurid  21183  minmar1val  21187  cramer  21230  cpmatel2  21251  m2cpm  21279  decpmatmul  21310  pmatcollpw1lem2  21313  pmatcollpw1  21314  pmatcollpw2lem  21315  pm2mpcl  21335  mply1topmatcl  21343  mp2pm2mplem2  21345  mp2pm2mplem4  21347  pm2mpghmlem2  21350  pm2mpghmlem1  21351  cayhamlem2  21422  neiint  21642  topssnei  21662  cnrest2  21824  cnprest2  21828  cnt0  21884  cnt1  21888  cnhaus  21892  cncmp  21930  fiuncmp  21942  sscmp  21943  hauscmp  21945  cnconn  21960  unconn  21967  comppfsc  22070  kgen2ss  22093  ptpjopn  22150  ptrescn  22177  qtopss  22253  kqfvima  22268  r0cld  22276  cmphaushmeo  22338  fbssint  22376  fbasrn  22422  filuni  22423  ufilmax  22445  fin1aufil  22470  fmf  22483  fmss  22484  rnelfmlem  22490  rnelfm  22491  fmufil  22497  fmco  22499  flimss2  22510  flimss1  22511  flimrest  22521  cnpflf2  22538  cnpflf  22539  flfcnp  22542  lmflf  22543  supnfcls  22558  fclsss1  22560  fclsss2  22561  cnpfcfi  22578  subgntr  22644  opnsubg  22645  cldsubg  22648  ustuqtop1  22779  ucncn  22823  bldisj  22937  blgt0  22938  bl2in  22939  blss2ps  22942  blss2  22943  xbln0  22953  blssps  22963  blss  22964  lpbl  23042  blcld  23044  blcls  23045  stdbdmopn  23057  metcnp2  23081  txmetcnp  23086  blval2  23101  restmetu  23109  nmoix  23267  nmoi2  23268  nmoeq0  23274  nmotri  23277  metdsge  23386  metds0  23387  metdseq0  23391  icoopnst  23472  iccpnfhmeo  23478  xrhmeo  23479  nmhmcn  23653  cphsqrtcl2  23719  cphsqrtcl3  23720  fmcfil  23804  bcthlem5  23860  cmetcusp1  23885  cssbn  23907  pjth  23971  ovolunnul  24030  volun  24075  voliunlem2  24081  itg2const  24270  iblconst  24347  itgconst  24348  limcvallem  24398  dvcnp2  24446  dvcn  24447  deg1mul3le  24639  deg1tmle  24640  ig1pdvds  24699  coe11  24772  dgrmulc  24790  dvply1  24802  aaliou2  24858  efcvx  24966  tanord  25049  logdivlti  25130  logccv  25173  recxpcl  25185  cxplea  25206  cxple2a  25209  ang180  25319  isosctrlem2  25324  cxp2lim  25482  amgm  25496  muval1  25638  dvdssqf  25643  mumullem2  25685  bcmono  25781  lgsneg  25825  lgsmod  25827  lgsdirprm  25835  lgsdir  25836  lgsdi  25838  brbtwn2  26619  colinearalglem1  26620  colinearalg  26624  axcgrtr  26629  axcontlem2  26679  upgrewlkle2  27316  wlksoneq1eq2  27374  crctcshwlkn0lem5  27520  wspthsnwspthsnon  27623  lppthon  27858  upgriseupth  27914  4cyclusnfrgr  27999  numclwwlk1lem2foa  28061  numclwwlk5  28095  nvmul0or  28355  shless  29064  shlej1  29065  pjspansn  29282  kbmul  29660  homco2  29682  kbass2  29822  fnpreimac  30345  padct  30382  eliccelico  30427  elicoelioo  30428  iocinioc2  30429  difioo  30432  swrdrn2  30556  swrdrn3  30557  xrge0npcan  30609  isarchi2  30742  archiabl  30755  lindssn  30867  mdetlap1  30991  pstmfval  31036  fmcncfil  31074  zrhnm  31110  qqhnm  31131  nexple  31168  volfiniune  31389  omsmeas  31481  eulerpartlemb  31526  probinc  31579  cndprob01  31593  signswmnd  31727  cvmsss2  32419  dvdspw  32880  funsseq  32909  frpomin  32976  frrlem10  33030  fprlem1  33035  sltres  33067  nolt02olem  33096  nolt02o  33097  nosupbnd1lem1  33106  nosupbnd1lem4  33109  nosupbnd1lem5  33110  nosupbnd1lem6  33111  cgrtriv  33361  5segofs  33365  btwntriv2  33371  btwnxfr  33415  segcon2  33464  brsegle2  33468  seglelin  33475  outsideofeu  33490  lindsenlbs  34769  mblfinlem2  34812  blbnd  34948  rrndstprj2  34992  zerdivemp1x  35108  lsmsat  36026  lsatfixedN  36027  lssat  36034  lkrlsp  36120  lshpkrlem4  36131  cvrcon3b  36295  leat3  36313  atlen0  36328  atnle  36335  atlatmstc  36337  atlatle  36338  cvlcvr1  36357  cvlsupr2  36361  hlsupr2  36405  hlrelat2  36421  cvrexchlem  36437  cvratlem  36439  lnnat  36445  atexchcvrN  36458  1cvratlt  36492  1cvrjat  36493  3atlem3  36503  3atlem7  36507  llni2  36530  atcvrlln2  36537  llnexatN  36539  llncmp  36540  2llnmat  36542  2at0mat0  36543  2atnelpln  36562  llncvrlpln2  36575  2lplnmN  36577  2llnmj  36578  lplncmp  36580  lplnexatN  36581  2llnjaN  36584  lvoli3  36595  islvol2aN  36610  4atlem3a  36615  4atlem4a  36617  4atlem4b  36618  4atlem11  36627  4atlem12  36630  lplncvrlvol2  36633  lvolcmp  36635  2lplnmj  36640  islinei  36758  linepmap  36793  lneq2at  36796  2llnma3r  36806  elpaddn0  36818  elpaddatriN  36821  elpaddat  36822  paddcom  36831  paddss1  36835  paddss2  36836  paddasslem6  36843  paddasslem7  36844  paddasslem10  36847  paddasslem15  36852  pmodlem2  36865  pmodl42N  36869  pmapjoin  36870  atmod1i1m  36876  llnmod1i2  36878  llnexchb2lem  36886  polcon2bN  36938  pclfinclN  36968  poml4N  36971  poml6N  36973  osumcllem11N  36984  osumclN  36985  pmapojoinN  36986  pexmidlem2N  36989  pexmidlem3N  36990  pexmidlem4N  36991  pexmidlem6N  36993  pexmidlem7N  36994  pl42lem2N  36998  pl42lem3N  36999  pl42lem4N  37000  pl42N  37001  lhpexle3lem  37029  lhpmcvr3  37043  lhp2at0nle  37053  lhprelat3N  37058  lauteq  37113  lautco  37115  ltrncoidN  37146  ltrneq2  37166  ltrnnidn  37192  ltrnideq  37193  trlnle  37204  cdlemc  37215  cdlemd4  37219  cdlemd5  37220  cdlemd9  37224  cdlemd  37225  ltrneq3  37226  cdlemefrs29pre00  37413  cdlemefrs29cpre1  37416  cdlemefrs29clN  37417  cdlemefrs32fva  37418  cdlemefr29exN  37420  cdlemefr27cl  37421  cdlemefs27cl  37431  cdlemefs32sn1aw  37432  cdleme32fva  37455  cdleme32d  37462  cdleme32f  37464  cdleme32le  37465  cdleme40n  37486  cdleme41snaw  37494  cdleme17d3  37514  cdleme48fvg  37518  cdlemeg46fvcl  37524  cdlemeg46fgN  37552  cdleme48fgv  37556  ltrniotavalbN  37602  cdlemb3  37624  cdlemg15  37674  cdlemg17dN  37681  trlco  37745  cdlemg44b  37750  ltrncom  37756  trljco  37758  tendococl  37790  tendoplcl  37799  tendoplcom  37800  tendotr  37848  cdlemk36  37931  cdlemk35s-id  37956  cdlemk39s-id  37958  cdlemk19x  37961  cdlemk53b  37974  cdlemk55  37979  cdlemk35u  37982  cdlemk55u  37984  cdlemk39u  37986  cdlemk19u  37988  cdlemk56  37989  tendoex  37993  cdleml5N  37998  dihord2pre  38243  dihord6apre  38274  dihord5b  38277  dihord5apre  38280  dihord  38282  dihmeetlem1N  38308  dihmeetlem2N  38317  dihglbcpreN  38318  dihmeetbN  38321  dihmeetlem4preN  38324  dihmeetlem5  38326  dihmeetlem6  38327  dihmeetlem7N  38328  dihmeetlem10N  38334  dihmeetlem11N  38335  dihmeetlem12N  38336  dihmeetlem13N  38337  dihmeetlem15N  38339  dihmeetlem17N  38341  dihmeetlem18N  38342  dihmeetlem19N  38343  dihmeetALTN  38345  dih1dimatlem0  38346  dihlspsnssN  38350  dvh3dim2  38466  resubcan2  39098  mzpsubst  39225  diophrw  39236  eldioph2lem1  39237  rencldnfi  39298  pellexlem2  39307  pellqrexplicit  39354  infmrgelbi  39355  rmxycomplete  39394  congadd  39443  acongeq  39460  jm2.19  39470  jm2.22  39472  jm2.20nn  39474  jm2.25lem1  39475  jm2.27  39485  jm3.1  39497  lmhmlnmsplit  39567  pwssplit4  39569  hbtlem2  39604  dgraa0p  39629  idomrootle  39675  proot1hash  39680  iocunico  39697  relexpxpmin  39942  brtrclfv2  39952  ntrclsk3  40300  grur1cld  40448  ismnu  40477  suprnmpt  41310  wessf1ornlem  41325  choicefi  41343  supxrgere  41481  supxrgelem  41485  supxrge  41486  infleinflem2  41519  snunioo1  41668  iccintsng  41679  fmul01  41741  lptre2pt  41801  0ellimcdiv  41810  fnlimfvre  41835  limsupmnfuzlem  41887  climisp  41907  limsupgtlem  41938  ibliccsinexp  42116  iblioosinexp  42118  volioc  42137  iblspltprt  42138  stoweidlem20  42186  stoweidlem22  42188  stoweidlem34  42200  stoweidlem44  42210  stoweidlem60  42226  wallispilem3  42233  fourierdlem42  42315  fourierdlem51  42323  fourierdlem54  42326  fourierdlem87  42359  fourierdlem97  42369  ioorrnopnlem  42470  sge0seq  42609  hoicvr  42711  submefmnd  43962  lincresunit3lem3  44427  lindssnlvec  44439  rrx2linesl  44628  line2  44637  itsclc0lem3  44643  itsclc0yqsollem1  44647  itscnhlc0xyqsol  44650  itschlc0xyqsol1  44651  itsclc0  44656  itscnhlinecirc02plem2  44668  itscnhlinecirc02plem3  44669
  Copyright terms: Public domain W3C validator