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

Theorem simpl2 1189
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 486 . 2 ((𝜓𝜃) → 𝜓)
213ad2antl2 1183 1 (((𝜑𝜓𝜒) ∧ 𝜃) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  w3a 1084
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 210  df-an 400  df-3an 1086
This theorem is referenced by:  simpl12  1246  simpl22  1249  simpl32  1252  simp1l2  1264  simp2l2  1270  simp3l2  1276  3anandirs  1469  rspc3ev  3588  2nreu  4352  f1prex  7022  weniso  7090  ofmpteq  7412  tfisi  7557  mposn  7785  smogt  7991  smorndom  7992  omeulem1  8195  nnmord  8245  nnmword  8246  difsnen  8586  enfixsn  8613  mapunen  8674  ac6sfi  8750  ordiso2  8967  wemaplem2  8999  wemapso  9003  wemapso2lem  9004  en2eqpr  9422  acndom  9466  infmap2  9633  cflim2  9678  cfsmolem  9685  coftr  9688  fin23lem26  9740  isf32lem9  9776  fin1a2lem9  9823  fin1a2lem10  9824  gchdomtri  10044  canth4  10062  gchpwdom  10085  gruima  10217  grudomon  10232  prn0  10404  distrlem4pr  10441  prlem934  10448  addcan  10817  addcan2  10818  divmulass  11314  divmulasscom  11315  ltmul1a  11482  supmul1  11601  uzsupss  12332  xaddass  12634  xleadd1a  12638  xlesubadd  12648  xmulass  12672  xlemul2a  12674  xadddilem  12679  xadddi  12680  ixxdisj  12745  ixxun  12746  ixxlb  12752  icoshftf1o  12856  icodisj  12858  ioounsn  12859  lincmb01cmp  12877  iccf1o  12878  elfz1b  12975  ssfzoulel  13130  modmuladd  13280  modaddmulmod  13305  ltexp2a  13530  leexp2  13535  ltexp2r  13537  exple1  13540  expnlbnd2  13595  mulsubdivbinom2  13622  fun2dmnop0  13852  ccatass  13937  ccatopth  14073  pfxccatin12lem2a  14084  repswpfx  14142  repswccat  14143  cshwidxmodr  14161  2cshw  14170  repsco  14197  s2f1o  14273  limsupgle  14830  limsupgre  14834  addcn2  14946  mulcn2  14948  binomrisefac  15392  dvdsval2  15606  dvdsadd2b  15652  dvdsmod  15674  oexpneg  15690  sadass  15814  gcdass  15889  rplpwr  15901  rppwr  15902  lcmass  15952  coprmdvds2  15992  rpmulgcd2  15994  rpdvds  15998  coprmprod  15999  cncongr2  16006  rpexp  16058  prmdiveq  16117  hashgcdlem  16119  odzdvds  16126  coprimeprodsq2  16140  pythagtriplem3  16149  pythagtriplem4  16150  pcdvdsb  16199  vdwnnlem1  16325  0ram  16350  ramz2  16354  ramub1lem1  16356  mremre  16871  mrieqv2d  16906  lubss  17727  lubun  17729  clatleglb  17732  clatglbss  17733  mrelatglb  17790  isnsgrp  17901  issubmnd  17934  gsumccatOLD  18001  gsumccat  18002  frmdss2  18024  submefmnd  18056  nmzsubg  18313  ghmnsgima  18378  gsmsymgreqlem1  18554  psgnunilem4  18621  odmodnn0  18664  odnncl  18669  odmod  18670  oddvds  18671  odeq  18674  odmulgid  18677  odmulgeq  18680  odbezout  18681  odf1o1  18693  odf1o2  18694  odngen  18698  gexdvdsi  18704  pgpfi1  18716  odcau  18725  subgslw  18737  fislw  18746  lsmless1x  18765  lsmless2x  18766  lsmsubm  18774  lsmmod  18797  lsmmod2  18798  efgsfo  18861  odadd1  18965  odadd2  18966  odadd  18967  lsmcomx  18973  prdscmnd  18978  gsumconst  19051  ablsimpgfindlem1  19226  srg1zr  19276  csrgbinom  19293  ring1eq0  19340  mulgass2  19351  cntzsubr  19565  isabvd  19588  rmodislmod  19699  0lmhm  19809  lmhmvsca  19814  reslmhm2b  19823  pwssplit1  19828  pwssplit2  19829  pwssplit3  19830  lbspss  19851  lspsnat  19914  lidldvgen  20025  xrsdsreclblem  20141  cssmre  20386  obs2ss  20422  uvcresum  20486  frlmsslsp  20489  frlmup4  20494  lindff1  20513  f1lindf  20515  lsslindf  20523  islindf4  20531  issubassa  20559  evlsval2  20763  coe1subfv  20899  coe1sclmul  20915  coe1sclmul2  20917  mpomatmul  21055  mamutpos  21067  scmatscmide  21116  mavmulsolcl  21160  mulmarep1gsum2  21183  mdetdiaglem  21207  mdetdiag  21208  mdetunilem1  21221  mdetunilem3  21223  mdetunilem9  21229  maducoeval2  21249  madurid  21253  slesolinvbi  21290  cramerimplem1  21292  cramerlem1  21296  cramer  21300  cpmatel2  21322  m2cpm  21350  m2pmfzmap  21356  m2cpminvid2lem  21363  m2cpminvid2  21364  decpmatmul  21381  pmatcollpw1lem2  21384  pmatcollpw1  21385  pmatcollpw2lem  21386  pmatcollpwfi  21391  pm2mpcl  21406  mply1topmatcl  21414  mp2pm2mplem2  21416  mp2pm2mplem4  21418  mp2pm2mplem5  21419  mp2pm2mp  21420  pm2mpghmlem2  21421  pm2mpghmlem1  21422  chfacfisfcpmat  21464  topssnei  21733  cnconst2  21892  cnpresti  21897  cnprest2  21899  cnpdis  21902  cnt0  21955  cnt1  21959  cnhaus  21963  sscmp  22014  hauscmp  22016  cnconn  22031  unconn  22038  finlocfin  22129  comppfsc  22141  kgen2ss  22164  ptpjopn  22221  prdstopn  22237  ptrescn  22248  qtopss  22324  kqfvima  22339  fbssint  22447  fbasrn  22493  filuni  22494  fmss  22555  rnelfm  22562  fmufil  22568  fmco  22570  flimss2  22581  flimss1  22582  flimrest  22592  cnpflf2  22609  flfcnp  22613  supnfcls  22629  fclsss1  22631  fclsss2  22632  isfcf  22643  subgntr  22716  opnsubg  22717  cldsubg  22720  ghmcnp  22724  ustuqtop1  22851  bldisj  23009  blgt0  23010  bl2in  23011  blss2ps  23014  blss2  23015  blssps  23035  blss  23036  xmetresbl  23048  lpbl  23114  blcld  23116  stdbdmopn  23129  metcnp3  23151  metcnp  23152  metcnp2  23153  txmetcnp  23158  blval2  23173  nmoix  23339  nmoi2  23340  nmotri  23349  metdsge  23458  metdseq0  23463  iocopnst  23549  xrhmeo  23555  nmhmcn  23729  cphsqrtcl2  23795  cphsqrtcl3  23796  cssbn  23983  pjth  24047  ovoliunlem2  24111  volun  24153  mbfimaopn2  24265  iblconst  24425  limcvallem  24478  dvfval  24504  dvcnp2  24527  dvcn  24528  deg1mul3le  24721  deg1tmle  24722  dvdsq1p  24765  ig1peu  24776  ig1pdvds  24781  ply1term  24805  coeid3  24841  dgrmulc  24872  dvply1  24884  aaliou2  24940  efcvx  25048  tanord  25134  eflogeq  25197  logdivlti  25215  logccv  25258  recxpcl  25270  cxplea  25291  cxpeq  25350  ang180  25404  isosctrlem2  25409  cxp2lim  25566  amgm  25580  muval1  25722  dvdssqf  25727  mumullem2  25769  mumul  25770  bcmono  25865  lgsneg  25909  lgsdilem  25912  lgsdirprm  25919  lgsdir  25920  lgsdi  25922  lgsne0  25923  brbtwn2  26703  colinearalglem1  26704  colinearalg  26708  axcgrtr  26713  axsegconlem8  26722  axsegconlem9  26723  axsegconlem10  26724  axcontlem2  26763  axcontlem10  26771  elntg2  26783  ewlkle  27399  crctcshwlkn0lem5  27604  wwlknp  27633  wwlksnext  27683  wwlksnextproplem1  27699  wspthsnwspthsnon  27706  clwlkclwwlklem3  27790  erclwwlksym  27810  erclwwlknsym  27859  upgriseupth  27996  eucrct2eupth  28034  3cyclfrgrrn  28075  numclwwlk2lem1lem  28131  numclwwlk1lem2foa  28143  frgrregord13  28185  nvmul0or  28437  ipval2lem2  28491  lnoadd  28545  lnosub  28546  lnomul  28547  shless  29146  shlej1  29147  kbmul  29742  homco2  29764  kbass2  29904  eliccelico  30530  elicoelioo  30531  iocinioc2  30532  iocinif  30534  difioo  30535  swrdrn2  30658  swrdrn3  30659  xrge0adddir  30730  xrge0npcan  30732  isarchi2  30868  archiabl  30881  rhmdvdsr  30946  pidlnz  30995  lindssn  30997  ssmxidl  31054  pstmfval  31253  fmcncfil  31288  zrhnm  31324  qqhnm  31345  nexple  31382  volfiniune  31603  dya2iocnrect  31653  probinc  31793  cndprob01  31807  signswmnd  31941  bnj517  32271  cvmsss2  32635  cvmlift2lem10  32673  br6  33107  funsseq  33125  fprlem1  33251  nolesgn2o  33292  nosep1o  33300  nosepssdm  33304  nosupres  33321  nosupbnd1lem1  33322  nosupbnd1lem4  33325  nosupbnd1lem5  33326  nosupbnd1lem6  33327  noetalem2  33332  cgrtriv  33577  5segofs  33581  btwnouttr2  33597  btwnxfr  33631  lineext  33651  btwnconn1lem13  33674  brsegle2  33684  nn0prpwlem  33784  lindsenlbs  35051  blbnd  35224  ismtyima  35240  rrndstprj2  35268  ghomdiv  35329  grpokerinj  35330  lsatfixedN  36304  lssat  36311  lshpkrlem4  36408  cvrcon3b  36572  atlen0  36605  atcvreq0  36609  atnle  36612  atlatmstc  36614  atlatle  36615  cvlcvr1  36634  hlsupr2  36682  hlrelat2  36698  cvrexchlem  36714  lnnat  36722  atcvrj2b  36727  3dimlem3  36756  3dim1  36762  1cvrjat  36770  llni  36803  llni2  36807  llnexatN  36816  2llnmat  36819  lplni  36827  2atnelpln  36839  llncvrlpln2  36852  2llnmj  36855  lplnexatN  36858  lplnexllnN  36859  2llnm3N  36864  lvoli  36870  lvoli3  36872  lvolnle3at  36877  islvol2aN  36887  4atlem4a  36894  4atlem4b  36895  4atlem11  36904  lplncvrlvol2  36910  2lplnmj  36917  islinei  37035  linepmap  37070  lnjatN  37075  lncvrat  37077  lncmp  37078  elpaddn0  37095  elpaddatriN  37098  elpaddat  37099  paddcom  37108  paddss2  37113  paddss12  37114  paddasslem4  37118  paddasslem9  37123  paddasslem10  37124  pmodl42N  37146  pmapjoin  37147  llnmod1i2  37155  polcon2bN  37215  pclfinclN  37245  poml4N  37248  poml6N  37250  osumcllem1N  37251  osumcllem2N  37252  osumcllem11N  37261  osumclN  37262  pmapojoinN  37263  pexmidlem2N  37266  pexmidlem3N  37267  pexmidlem4N  37268  pexmidlem6N  37270  pexmidlem7N  37271  pl42lem2N  37275  pl42lem3N  37276  pl42lem4N  37277  pl42N  37278  lhprelat3N  37335  4atex  37371  lauteq  37390  lautco  37392  ltrncoidN  37423  ltrneq2  37443  ltrnideq  37470  trlnle  37481  trlval3  37482  cdlemc  37492  cdlemd9  37501  cdlemd  37502  cdleme21j  37631  cdleme21  37632  cdleme29ex  37669  cdlemefr27cl  37698  cdlemefs27cl  37708  cdleme32d  37739  cdleme32f  37741  cdleme35h2  37752  cdleme40m  37762  cdleme17d3  37791  cdleme48fvg  37795  cdlemeg46fvcl  37801  cdlemeg46fgN  37829  cdleme48fgv  37833  cdleme50trn3  37848  cdlemb3  37901  cdlemg8  37926  cdlemg11a  37932  cdlemg15a  37950  cdlemg15  37951  cdlemg16  37952  cdlemg16z  37954  cdlemg17dN  37958  cdlemg24  37983  cdlemg37  37984  cdlemg29  38000  cdlemg33b  38002  cdlemg38  38010  cdlemg40  38012  trlco  38022  cdlemg44b  38027  ltrncom  38033  trljco  38035  tendococl  38067  tendoplcl  38076  tendoplcom  38077  cdlemj2  38117  tendoid0  38120  tendo1ne0  38123  cdlemk25-3  38199  cdlemk36  38208  cdlemkid4  38229  cdlemk19x  38238  cdlemk53  38252  cdlemk56  38266  cdleml5N  38275  tendospcanN  38318  cdlemm10N  38413  dihord6apre  38551  dihord  38559  dihmeetlem1N  38585  dihglblem2N  38589  dihmeetlem2N  38594  dihmeetbN  38598  dihmeetlem5  38603  dihmeetlem6  38604  dihmeetlem7N  38605  dihmeetlem10N  38611  dihmeetlem12N  38613  dihmeetlem16N  38617  dihmeetlem17N  38618  dihmeetlem18N  38619  dihmeetALTN  38622  dihlspsnssN  38627  dvh3dim2  38743  dvh3dim3N  38744  lcfrlem16  38853  mapdrvallem2  38940  mapdh8ad  39074  hgmapvvlem3  39220  resubcan2  39519  diophrw  39693  eldioph2lem1  39694  diophrex  39709  rencldnfi  39755  pellexlem2  39764  pellqrexplicit  39811  infmrgelbi  39812  pellfundglb  39819  pellfund14gap  39821  rmxycomplete  39851  congadd  39900  acongeq  39917  jm2.19  39927  jm2.23  39930  jm2.20nn  39931  jm2.27  39942  jm3.1  39954  lnmepi  40022  lmhmlnmsplit  40024  hbtlem2  40061  dgraa0p  40086  idomrootle  40132  proot1hash  40137  iocunico  40154  iocinico  40155  relexpxpmin  40411  ntrclsk3  40766  grur1cld  40933  ismnu  40962  grumnudlem  40986  rfcnnnub  41658  uzwo4  41680  wessf1ornlem  41804  supxrge  41963  infleinflem2  41996  iccintsng  42153  climsuse  42243  lptre2pt  42275  limcleqr  42279  0ellimcdiv  42284  fnlimfvre  42309  dvnprodlem1  42581  volioc  42607  stoweidlem17  42652  stoweidlem19  42654  stoweidlem20  42655  stoweidlem22  42657  stoweidlem28  42663  stoweidlem34  42669  stoweidlem44  42679  stoweidlem60  42695  wallispilem3  42702  fourierdlem42  42784  fourierdlem48  42789  fourierdlem51  42792  fourierdlem54  42795  fourierdlem74  42815  fourierdlem77  42818  fourierdlem87  42828  fourierdlem97  42838  ioorrnopnlem  42939  ovnsubaddlem2  43203  smfinflem  43441  eluzge0nn0  43862  fzopredsuc  43873  fzoopth  43877  imasetpreimafvbijlemfv  43912  lighneallem4  44121  oexpnegALTV  44188  oexpnegnz  44189  tgblthelfgott  44326  rmsupp0  44763  rmsuppss  44765  lincresunit3lem3  44876  lincresunit3lem2  44882  lindssnlvec  44888  fdivmptf  44948  refdivmptf  44949  elbigolo1  44964  rrx2linest  45149  itsclc0lem1  45163  itsclc0lem2  45164  itsclc0yqsollem1  45169  itsclc0b  45179
  Copyright terms: Public domain W3C validator