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

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

Proof of Theorem simpl2
StepHypRef Expression
1 simpl 483 . 2 ((𝜓𝜃) → 𝜓)
213ad2antl2 1178 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:  simpl12  1241  simpl22  1244  simpl32  1247  simp1l2  1259  simp2l2  1265  simp3l2  1271  3anandirs  1463  rspc3ev  3636  2nreu  4391  f1prex  7031  weniso  7096  ofmpteq  7417  tfisi  7561  mposn  7789  smogt  7995  smorndom  7996  omeulem1  8198  nnmord  8248  nnmword  8249  difsnen  8588  enfixsn  8615  mapunen  8675  ac6sfi  8751  ordiso2  8968  wemaplem2  9000  wemapso  9004  wemapso2lem  9005  en2eqpr  9422  acndom  9466  infmap2  9629  cflim2  9674  cfsmolem  9681  coftr  9684  fin23lem26  9736  isf32lem9  9772  fin1a2lem9  9819  fin1a2lem10  9820  gchdomtri  10040  canth4  10058  gchpwdom  10081  gruima  10213  grudomon  10228  prn0  10400  distrlem4pr  10437  prlem934  10444  addcan  10813  addcan2  10814  divmulass  11310  divmulasscom  11311  ltmul1a  11478  supmul1  11599  uzsupss  12329  xaddass  12632  xleadd1a  12636  xlesubadd  12646  xmulass  12670  xlemul2a  12672  xadddilem  12677  xadddi  12678  ixxdisj  12743  ixxun  12744  ixxlb  12750  icoshftf1o  12850  icodisj  12852  ioounsn  12853  lincmb01cmp  12871  iccf1o  12872  elfz1b  12966  ssfzoulel  13121  modmuladd  13271  modaddmulmod  13296  ltexp2a  13520  leexp2  13525  ltexp2r  13527  exple1  13530  expnlbnd2  13585  mulsubdivbinom2  13612  fun2dmnop0  13842  ccatass  13932  ccatopth  14068  pfxccatin12lem2a  14079  repswpfx  14137  repswccat  14138  cshwidxmodr  14156  2cshw  14165  repsco  14192  s2f1o  14268  limsupgle  14824  limsupgre  14828  addcn2  14940  mulcn2  14942  binomrisefac  15386  dvdsval2  15600  dvdsadd2b  15646  dvdsmod  15668  oexpneg  15684  sadass  15810  gcdass  15885  rplpwr  15897  rppwr  15898  lcmass  15948  coprmdvds2  15988  rpmulgcd2  15990  rpdvds  15994  coprmprod  15995  cncongr2  16002  rpexp  16054  prmdiveq  16113  hashgcdlem  16115  odzdvds  16122  coprimeprodsq2  16136  pythagtriplem3  16145  pythagtriplem4  16146  pcdvdsb  16195  vdwnnlem1  16321  0ram  16346  ramz2  16350  ramub1lem1  16352  mremre  16865  mrieqv2d  16900  lubss  17721  lubun  17723  clatleglb  17726  clatglbss  17727  mrelatglb  17784  isnsgrp  17895  issubmnd  17928  gsumccatOLD  17995  gsumccat  17996  frmdss2  18018  nmzsubg  18257  ghmnsgima  18322  gsmsymgreqlem1  18489  psgnunilem4  18556  odmodnn0  18599  odnncl  18604  odmod  18605  oddvds  18606  odeq  18609  odmulgid  18612  odmulgeq  18615  odbezout  18616  odf1o1  18628  odf1o2  18629  odngen  18633  gexdvdsi  18639  pgpfi1  18651  odcau  18660  subgslw  18672  fislw  18681  lsmless1x  18700  lsmless2x  18701  lsmsubm  18709  lsmmod  18732  lsmmod2  18733  efgsfo  18796  odadd1  18899  odadd2  18900  odadd  18901  lsmcomx  18907  prdscmnd  18912  gsumconst  18985  ablsimpgfindlem1  19160  srg1zr  19210  csrgbinom  19227  ring1eq0  19271  mulgass2  19282  cntzsubr  19499  isabvd  19522  rmodislmod  19633  0lmhm  19743  lmhmvsca  19748  reslmhm2b  19757  pwssplit1  19762  pwssplit2  19763  pwssplit3  19764  lbspss  19785  lspsnat  19848  lidldvgen  19958  issubassa  20028  evlsval2  20230  coe1subfv  20364  coe1sclmul  20380  coe1sclmul2  20382  xrsdsreclblem  20521  cssmre  20767  obs2ss  20803  uvcresum  20867  frlmsslsp  20870  frlmup4  20875  lindff1  20894  f1lindf  20896  lsslindf  20904  islindf4  20912  mpomatmul  20985  mamutpos  20997  scmatscmide  21046  mavmulsolcl  21090  mulmarep1gsum2  21113  mdetdiaglem  21137  mdetdiag  21138  mdetunilem1  21151  mdetunilem3  21153  mdetunilem9  21159  maducoeval2  21179  madurid  21183  slesolinvbi  21220  cramerimplem1  21222  cramerlem1  21226  cramer  21230  cpmatel2  21251  m2cpm  21279  m2pmfzmap  21285  m2cpminvid2lem  21292  m2cpminvid2  21293  decpmatmul  21310  pmatcollpw1lem2  21313  pmatcollpw1  21314  pmatcollpw2lem  21315  pmatcollpwfi  21320  pm2mpcl  21335  mply1topmatcl  21343  mp2pm2mplem2  21345  mp2pm2mplem4  21347  mp2pm2mplem5  21348  mp2pm2mp  21349  pm2mpghmlem2  21350  pm2mpghmlem1  21351  chfacfisfcpmat  21393  topssnei  21662  cnconst2  21821  cnpresti  21826  cnprest2  21828  cnpdis  21831  cnt0  21884  cnt1  21888  cnhaus  21892  sscmp  21943  hauscmp  21945  cnconn  21960  unconn  21967  finlocfin  22058  comppfsc  22070  kgen2ss  22093  ptpjopn  22150  prdstopn  22166  ptrescn  22177  qtopss  22253  kqfvima  22268  fbssint  22376  fbasrn  22422  filuni  22423  fmss  22484  rnelfm  22491  fmufil  22497  fmco  22499  flimss2  22510  flimss1  22511  flimrest  22521  cnpflf2  22538  flfcnp  22542  supnfcls  22558  fclsss1  22560  fclsss2  22561  isfcf  22572  subgntr  22644  opnsubg  22645  cldsubg  22648  ghmcnp  22652  ustuqtop1  22779  bldisj  22937  blgt0  22938  bl2in  22939  blss2ps  22942  blss2  22943  blssps  22963  blss  22964  xmetresbl  22976  lpbl  23042  blcld  23044  stdbdmopn  23057  metcnp3  23079  metcnp  23080  metcnp2  23081  txmetcnp  23086  blval2  23101  nmoix  23267  nmoi2  23268  nmotri  23277  metdsge  23386  metdseq0  23391  iocopnst  23473  xrhmeo  23479  nmhmcn  23653  cphsqrtcl2  23719  cphsqrtcl3  23720  cssbn  23907  pjth  23971  ovoliunlem2  24033  volun  24075  mbfimaopn2  24187  iblconst  24347  limcvallem  24398  dvfval  24424  dvcnp2  24446  dvcn  24447  deg1mul3le  24639  deg1tmle  24640  dvdsq1p  24683  ig1peu  24694  ig1pdvds  24699  ply1term  24723  coeid3  24759  dgrmulc  24790  dvply1  24802  aaliou2  24858  efcvx  24966  tanord  25049  eflogeq  25112  logdivlti  25130  logccv  25173  recxpcl  25185  cxplea  25206  cxpeq  25265  ang180  25319  isosctrlem2  25324  cxp2lim  25482  amgm  25496  muval1  25638  dvdssqf  25643  mumullem2  25685  mumul  25686  bcmono  25781  lgsneg  25825  lgsdilem  25828  lgsdirprm  25835  lgsdir  25836  lgsdi  25838  lgsne0  25839  brbtwn2  26619  colinearalglem1  26620  colinearalg  26624  axcgrtr  26629  axsegconlem8  26638  axsegconlem9  26639  axsegconlem10  26640  axcontlem2  26679  axcontlem10  26687  elntg2  26699  ewlkle  27315  crctcshwlkn0lem5  27520  wwlknp  27549  wwlksnext  27599  wwlksnextproplem1  27616  wspthsnwspthsnon  27623  clwlkclwwlklem3  27707  erclwwlksym  27727  erclwwlknsym  27777  upgriseupth  27914  eucrct2eupth  27952  3cyclfrgrrn  27993  numclwwlk2lem1lem  28049  numclwwlk1lem2foa  28061  frgrregord13  28103  nvmul0or  28355  ipval2lem2  28409  lnoadd  28463  lnosub  28464  lnomul  28465  shless  29064  shlej1  29065  kbmul  29660  homco2  29682  kbass2  29822  eliccelico  30427  elicoelioo  30428  iocinioc2  30429  iocinif  30431  difioo  30432  swrdrn2  30556  swrdrn3  30557  xrge0adddir  30607  xrge0npcan  30609  isarchi2  30742  archiabl  30755  rhmdvdsr  30819  lindssn  30867  pstmfval  31036  fmcncfil  31074  zrhnm  31110  qqhnm  31131  nexple  31168  volfiniune  31389  dya2iocnrect  31439  probinc  31579  cndprob01  31593  signswmnd  31727  bnj517  32057  cvmsss2  32419  cvmlift2lem10  32457  br6  32891  funsseq  32909  fprlem1  33035  nolesgn2o  33076  nosep1o  33084  nosepssdm  33088  nosupres  33105  nosupbnd1lem1  33106  nosupbnd1lem4  33109  nosupbnd1lem5  33110  nosupbnd1lem6  33111  noetalem2  33116  cgrtriv  33361  5segofs  33365  btwnouttr2  33381  btwnxfr  33415  lineext  33435  btwnconn1lem13  33458  brsegle2  33468  nn0prpwlem  33568  lindsenlbs  34769  blbnd  34948  ismtyima  34964  rrndstprj2  34992  ghomdiv  35053  grpokerinj  35054  lsatfixedN  36027  lssat  36034  lshpkrlem4  36131  cvrcon3b  36295  atlen0  36328  atcvreq0  36332  atnle  36335  atlatmstc  36337  atlatle  36338  cvlcvr1  36357  hlsupr2  36405  hlrelat2  36421  cvrexchlem  36437  lnnat  36445  atcvrj2b  36450  3dimlem3  36479  3dim1  36485  1cvrjat  36493  llni  36526  llni2  36530  llnexatN  36539  2llnmat  36542  lplni  36550  2atnelpln  36562  llncvrlpln2  36575  2llnmj  36578  lplnexatN  36581  lplnexllnN  36582  2llnm3N  36587  lvoli  36593  lvoli3  36595  lvolnle3at  36600  islvol2aN  36610  4atlem4a  36617  4atlem4b  36618  4atlem11  36627  lplncvrlvol2  36633  2lplnmj  36640  islinei  36758  linepmap  36793  lnjatN  36798  lncvrat  36800  lncmp  36801  elpaddn0  36818  elpaddatriN  36821  elpaddat  36822  paddcom  36831  paddss2  36836  paddss12  36837  paddasslem4  36841  paddasslem9  36846  paddasslem10  36847  pmodl42N  36869  pmapjoin  36870  llnmod1i2  36878  polcon2bN  36938  pclfinclN  36968  poml4N  36971  poml6N  36973  osumcllem1N  36974  osumcllem2N  36975  osumcllem11N  36984  osumclN  36985  pmapojoinN  36986  pexmidlem2N  36989  pexmidlem3N  36990  pexmidlem4N  36991  pexmidlem6N  36993  pexmidlem7N  36994  pl42lem2N  36998  pl42lem3N  36999  pl42lem4N  37000  pl42N  37001  lhprelat3N  37058  4atex  37094  lauteq  37113  lautco  37115  ltrncoidN  37146  ltrneq2  37166  ltrnideq  37193  trlnle  37204  trlval3  37205  cdlemc  37215  cdlemd9  37224  cdlemd  37225  cdleme21j  37354  cdleme21  37355  cdleme29ex  37392  cdlemefr27cl  37421  cdlemefs27cl  37431  cdleme32d  37462  cdleme32f  37464  cdleme35h2  37475  cdleme40m  37485  cdleme17d3  37514  cdleme48fvg  37518  cdlemeg46fvcl  37524  cdlemeg46fgN  37552  cdleme48fgv  37556  cdleme50trn3  37571  cdlemb3  37624  cdlemg8  37649  cdlemg11a  37655  cdlemg15a  37673  cdlemg15  37674  cdlemg16  37675  cdlemg16z  37677  cdlemg17dN  37681  cdlemg24  37706  cdlemg37  37707  cdlemg29  37723  cdlemg33b  37725  cdlemg38  37733  cdlemg40  37735  trlco  37745  cdlemg44b  37750  ltrncom  37756  trljco  37758  tendococl  37790  tendoplcl  37799  tendoplcom  37800  cdlemj2  37840  tendoid0  37843  tendo1ne0  37846  cdlemk25-3  37922  cdlemk36  37931  cdlemkid4  37952  cdlemk19x  37961  cdlemk53  37975  cdlemk56  37989  cdleml5N  37998  tendospcanN  38041  cdlemm10N  38136  dihord6apre  38274  dihord  38282  dihmeetlem1N  38308  dihglblem2N  38312  dihmeetlem2N  38317  dihmeetbN  38321  dihmeetlem5  38326  dihmeetlem6  38327  dihmeetlem7N  38328  dihmeetlem10N  38334  dihmeetlem12N  38336  dihmeetlem16N  38340  dihmeetlem17N  38341  dihmeetlem18N  38342  dihmeetALTN  38345  dihlspsnssN  38350  dvh3dim2  38466  dvh3dim3N  38467  lcfrlem16  38576  mapdrvallem2  38663  mapdh8ad  38797  hgmapvvlem3  38943  resubcan2  39098  diophrw  39236  eldioph2lem1  39237  diophrex  39252  rencldnfi  39298  pellexlem2  39307  pellqrexplicit  39354  infmrgelbi  39355  pellfundglb  39362  pellfund14gap  39364  rmxycomplete  39394  congadd  39443  acongeq  39460  jm2.19  39470  jm2.23  39473  jm2.20nn  39474  jm2.27  39485  jm3.1  39497  lnmepi  39565  lmhmlnmsplit  39567  hbtlem2  39604  dgraa0p  39629  idomrootle  39675  proot1hash  39680  iocunico  39697  iocinico  39698  relexpxpmin  39942  ntrclsk3  40300  grur1cld  40448  ismnu  40477  grumnudlem  40501  rfcnnnub  41173  uzwo4  41195  wessf1ornlem  41325  supxrge  41486  infleinflem2  41519  iccintsng  41679  climsuse  41769  lptre2pt  41801  limcleqr  41805  0ellimcdiv  41810  fnlimfvre  41835  dvnprodlem1  42111  volioc  42137  stoweidlem17  42183  stoweidlem19  42185  stoweidlem20  42186  stoweidlem22  42188  stoweidlem28  42194  stoweidlem34  42200  stoweidlem44  42210  stoweidlem60  42226  wallispilem3  42233  fourierdlem42  42315  fourierdlem48  42320  fourierdlem51  42323  fourierdlem54  42326  fourierdlem74  42346  fourierdlem77  42349  fourierdlem87  42359  fourierdlem97  42369  ioorrnopnlem  42470  ovnsubaddlem2  42734  smfinflem  42972  eluzge0nn0  43393  fzopredsuc  43404  fzoopth  43408  lighneallem4  43622  oexpnegALTV  43689  oexpnegnz  43690  tgblthelfgott  43827  submefmnd  43962  rmsupp0  44314  rmsuppss  44316  lincresunit3lem3  44427  lincresunit3lem2  44433  lindssnlvec  44439  fdivmptf  44499  refdivmptf  44500  elbigolo1  44515  rrx2linest  44627  itsclc0lem1  44641  itsclc0lem2  44642  itsclc0yqsollem1  44647  itsclc0b  44657
  Copyright terms: Public domain W3C validator