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

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

Proof of Theorem simpl1
StepHypRef Expression
1 simpl 483 . 2 ((𝜑𝜃) → 𝜑)
213ad2antl1 1177 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:  simpl11  1240  simpl21  1243  simpl31  1246  simp1l1  1258  simp2l1  1264  simp3l1  1270  3anandirs  1463  rspc3ev  3636  2nreu  4391  f1prex  7031  cocan1  7038  weniso  7096  smogt  7995  smorndom  7996  omeulem1  8198  nnmord  8248  nnmword  8249  difsnen  8588  enfixsn  8615  mapunen  8675  ac6sfi  8751  fipreima  8819  elfiun  8883  ordiso2  8968  wemaplem2  9000  wemapso  9004  en2eqpr  9422  indcardi  9456  fodomfi2  9475  iunfictbso  9529  infmap2  9629  cofsmo  9680  cfsmolem  9681  coftr  9684  fin23lem11  9728  fincssdom  9734  fin23lem26  9736  isf32lem9  9772  ac6num  9890  gchdomtri  10040  gchpwdom  10081  winainflem  10104  tskuni  10194  gruima  10213  gruf  10222  grudomon  10228  elnpi  10399  distrlem4pr  10437  prlem934  10444  addcan  10813  addcan2  10814  divmulass  11310  divmulasscom  11311  ltmul1a  11478  suprleub  11596  supmul1  11599  suprzcl  12051  uzsupss  12329  xleadd1a  12636  xlesubadd  12646  xmulasslem3  12669  xlemul2a  12672  xadddilem  12677  xadddi2  12680  ixxun  12744  icoshftf1o  12850  ioounsn  12853  snunioc  12856  lincmb01cmp  12871  iccf1o  12872  nn0p1elfzo  13070  fzofzim  13074  ltexp2a  13520  leexp2  13525  ltexp2r  13527  exple1  13530  expnlbnd2  13585  fun2dmnop0  13842  ccatass  13932  ccat2s1fvwOLD  13989  swrdswrdlem  14056  ccatopth  14068  repswpfx  14137  2cshw  14165  cshimadifsn  14181  cshimadifsn0  14182  cshco  14188  repsco  14192  s2f1o  14268  limsupgre  14828  addcn2  14940  mulcn2  14942  ntrivcvgmul  15248  binomrisefac  15386  dvdsmodexp  15605  dvdsadd2b  15646  dvdsmod  15668  oexpneg  15684  sadass  15810  gcdass  15885  rplpwr  15897  rppwr  15898  lcmfunsnlem1  15971  coprmdvds2  15988  rpmulgcd2  15990  qredeq  15991  rpdvds  15994  cncongr2  16002  rpexp  16054  prmdiveq  16113  hashgcdlem  16115  odzdvds  16122  modprmn0modprm0  16134  coprimeprodsq2  16136  pythagtriplem3  16145  pcdvdsb  16195  pcgcd1  16203  qexpz  16227  pockthg  16232  vdwnnlem1  16321  0ram  16346  ramz2  16350  lubss  17721  lubun  17723  clatleglb  17726  clatglbss  17727  mrelatglb  17784  isnsgrp  17895  issubmnd  17928  ress0g  17929  gsumccatOLD  17995  gsumccat  17996  frmdss2  18018  mulgneg  18186  mulgdirlem  18198  submmulg  18211  subgmulg  18233  nmzsubg  18257  ghmmulg  18310  gsmsymgreqlem1  18489  pmtrfb  18524  psgnunilem4  18556  odmodnn0  18599  odnncl  18604  odmod  18605  odmulgid  18612  odmulgeq  18615  odf1o1  18628  odf1o2  18629  odngen  18633  gexdvdsi  18639  pgpfi1  18651  odcau  18660  subgslw  18672  fislw  18681  lsmssv  18699  lsmless1x  18700  lsmless2x  18701  lsmsubm  18709  lsmmod  18732  lsmmod2  18733  efgred  18805  cntzcmn  18891  ghmplusg  18897  odadd1  18899  odadd2  18900  odadd  18901  lsmcomx  18907  gsumconst  18985  ablsimpgprmd  19168  srg1zr  19210  ring1eq0  19271  mulgass2  19282  isabvd  19522  rmodislmodlem  19632  rmodislmod  19633  lssintcl  19667  0lmhm  19743  lmhmvsca  19748  reslmhm2b  19757  pwssplit1  19762  pwssplit3  19764  lspfixed  19831  lspsnat  19848  lidldvgen  19958  issubassa  20028  evlsval2  20230  psrplusgpropd  20334  coe1subfv  20364  coe1mul2  20367  xrsdsreclblem  20521  regsumsupp  20696  obselocv  20802  uvcresum  20867  frlmsslsp  20870  frlmup4  20875  lindff1  20894  f1lindf  20896  lsslindf  20904  islindf4  20912  lbslcic  20915  mhmvlin  20938  mpomatmul  20985  mamutpos  20997  scmatscmide  21046  mavmulsolcl  21090  marrepcl  21103  mdetdiag  21138  mdetunilem1  21151  mdetunilem3  21153  mdetunilem7  21157  mdetunilem9  21159  mdetmul  21162  slesolinvbi  21220  m2pmfzmap  21285  pmatcollpwlem  21318  pmatcollpw  21319  mp2pm2mplem4  21347  chpdmatlem3  21378  chfacfisfcpmat  21393  chfacfscmulgsum  21398  chfacfpmmulgsum  21402  chfacfpmmulgsum2  21403  cayhamlem1  21404  cpmidpmatlem2  21409  cpmadugsumlemB  21412  cpmadugsumlemC  21413  cpmadugsumlemF  21414  riinopn  21446  neiint  21642  topssnei  21662  restntr  21720  iscnp4  21801  cnconst2  21821  cnrest2  21824  cnprest2  21828  cnpdis  21831  cnt0  21884  cnt1  21888  cnhaus  21892  ordthauslem  21921  cncmp  21930  fiuncmp  21942  sscmp  21943  hauscmp  21945  cnconn  21960  unconn  21967  nlly2i  22014  llynlly  22015  nllyidm  22027  finlocfin  22058  ptrescn  22177  xkococnlem  22197  qtopss  22253  kqfvima  22268  r0cld  22276  ordthmeolem  22339  fbssint  22376  fmf  22483  fmss  22484  elfm  22485  rnelfmlem  22490  rnelfm  22491  fmco  22499  flimss2  22510  flimss1  22511  flimrest  22521  flftg  22534  cnpflf2  22538  cnpflf  22539  flfcnp  22542  supnfcls  22558  fclsss1  22560  fclsss2  22561  fcfnei  22573  fcfelbas  22574  cnpfcfi  22578  subgntr  22644  opnsubg  22645  cldsubg  22648  ghmcnp  22652  utop2nei  22788  neipcfilu  22834  bldisj  22937  blgt0  22938  bl2in  22939  blss2ps  22942  blss2  22943  blssps  22963  blss  22964  xmetresbl  22976  lpbl  23042  blcld  23044  stdbdbl  23056  metcnp3  23079  metcnp2  23081  txmetcnp  23086  blval2  23101  nmoix  23267  nmoeq0  23274  icoopnst  23472  iocopnst  23473  xrhmeo  23479  nmhmcn  23653  cphsqrtcl2  23719  cphsqrtcl3  23720  cfil3i  23801  caublcls  23841  bcthlem5  23860  cmetcusp1  23885  cssbn  23907  rrxcph  23924  pjth  23971  ovoliunlem2  24033  volun  24075  volsup2  24135  mbfimaopn2  24187  iblconst  24347  itgconst  24348  dvcnp2  24446  dvcn  24447  deg1mul3le  24639  deg1tmle  24640  dvdsq1p  24683  ig1peu  24694  ig1pdvds  24699  coeid3  24759  dgrmulc  24790  efcvx  24966  tanord  25049  logdivlti  25130  logccv  25173  recxpcl  25185  cxpeq  25265  ang180  25319  isosctrlem2  25324  cxp2lim  25482  amgm  25496  muval1  25638  dvdssqf  25643  mumullem2  25685  mumul  25686  bcmono  25781  lgsfcl2  25807  lgsdilem  25828  lgsdirprm  25835  lgsdir  25836  lgsdi  25838  lgsne0  25839  padicabv  26134  brbtwn2  26619  colinearalglem1  26620  colinearalg  26624  axcgrtr  26629  axsegconlem8  26638  axsegconlem9  26639  axsegconlem10  26640  axcontlem8  26685  axcontlem10  26687  elntg2  26699  vtxdlfuhgr1v  27189  umgr2wlk  27656  erclwwlksym  27727  clwwlkfo  27757  clwwlkext2edg  27763  erclwwlknsym  27777  clwwlknon1  27804  numclwwlk2lem1  28083  numclwwlk5  28095  frgrregord13  28103  nvmul0or  28355  ipval2lem2  28409  lnomul  28465  shless  29064  shlej1  29065  pjspansn  29282  hoadddi  29508  kbmul  29660  homco2  29682  kbass2  29822  eliccelico  30427  elicoelioo  30428  iocinioc2  30429  iocinif  30431  swrdrn2  30556  xrge0adddir  30607  xrge0npcan  30609  archiabl  30755  ress1r  30788  rhmdvdsr  30819  pstmfval  31036  fmcncfil  31074  zrhnm  31110  qqhnm  31131  measvunilem  31371  volfiniune  31389  dya2iocnrect  31439  sibfinima  31497  probun  31577  probinc  31579  cndprob01  31593  signstfvp  31741  bnj517  32057  bnj594  32084  pconnpi1  32382  cvmsss2  32419  mrsubcv  32655  msubvrs  32705  dvdspw  32880  br6  32891  br4  32892  frpomin  32976  frrlem4  33024  frrlem10  33030  fprlem1  33035  nosep1o  33084  nosepssdm  33088  nolt02olem  33096  nosupres  33105  nosupbnd1lem1  33106  nosupbnd1lem4  33109  nosupbnd1lem5  33110  nosupbnd1lem6  33111  nosupbnd2  33114  noetalem2  33116  cgrcomim  33348  cgrtriv  33361  cgrextend  33367  segconeq  33369  btwntriv2  33371  btwnintr  33378  btwnexch3  33379  btwnouttr2  33381  trisegint  33387  cgrsub  33404  cgrxfr  33414  btwnxfr  33415  lineext  33435  btwnconn1lem13  33458  btwnconn1lem14  33459  btwnconn3  33462  segcon2  33464  brsegle  33467  brsegle2  33468  segletr  33473  segleantisym  33474  seglelin  33475  outsideofeu  33490  lineunray  33506  lineelsb2  33507  ivthALT  33581  lindsenlbs  34769  areacirc  34869  cocanfo  34876  upixp  34887  ismtyima  34964  rrndstprj2  34992  zerdivemp1x  35108  lsatfixedN  36027  lssat  36034  eqlkr  36117  eqlkr2  36118  lkrlsp  36120  lshpkrlem4  36131  opposet  36199  cvrcon3b  36295  cvrcmp  36301  atlen0  36328  atnle  36335  atlatmstc  36337  cvlatexch3  36356  cvlsupr2  36361  hlsupr2  36405  hlrelat2  36421  cvrexchlem  36437  lnnat  36445  atcvrj2b  36450  atle  36454  atexchcvrN  36458  atbtwn  36464  athgt  36474  3dimlem3  36479  3dim1  36485  1cvratlt  36492  1cvrjat  36493  ps-1  36495  ps-2  36496  3atlem3  36503  3atlem5  36505  3atlem7  36507  llni  36526  llni2  36530  atcvrlln2  36537  llnexatN  36539  llncmp  36540  2llnmat  36542  2at0mat0  36543  lplni  36550  lplnnle2at  36559  2atnelpln  36562  lplnllnneN  36574  llncvrlpln2  36575  2lplnmN  36577  2llnmj  36578  lplncmp  36580  lplnexatN  36581  lplnexllnN  36582  2llnm3N  36587  lvoli  36593  lvoli3  36595  islvol2aN  36610  4atlem0a  36611  4atlem3  36614  4atlem3a  36615  4atlem4a  36617  4atlem4b  36618  4atlem4c  36619  4atlem4d  36620  4atlem10b  36623  4atlem11  36627  4atlem12  36630  lplncvrlvol2  36633  lvolcmp  36635  2lplnmj  36640  islinei  36758  pmapglbx  36787  linepmap  36793  lneq2at  36796  lnjatN  36798  lncvrat  36800  lncmp  36801  2llnma3r  36806  elpaddatriN  36821  elpaddat  36822  paddcom  36831  paddss1  36835  paddss2  36836  paddss12  36837  paddasslem6  36843  paddasslem7  36844  paddasslem8  36845  paddasslem9  36846  paddasslem15  36852  pmodlem2  36865  pmodl42N  36869  pmapjoin  36870  llnmod1i2  36878  2polcon4bN  36936  polcon2bN  36938  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  lhpexle2lem  37027  lhpexle3lem  37029  lhpexle3  37030  lhpmcvr3  37043  lhp2at0nle  37053  lhprelat3N  37058  4atex  37094  4atex2  37095  lauteq  37113  lautco  37115  ltrncoidN  37146  ltrneq2  37166  ltrnnidn  37192  ltrnideq  37193  trlnid  37197  ltrnatlw  37201  trlnle  37204  trlval3  37205  trlval4  37206  cdlemc  37215  cdlemd5  37220  cdlemd9  37224  ltrneq3  37226  cdleme0moN  37243  cdleme20  37342  cdleme21j  37354  cdleme21  37355  cdleme27cl  37384  cdlemefrs29bpre0  37414  cdlemefs27cl  37431  cdlemefs32sn1aw  37432  cdleme43fsv1snlem  37438  cdleme32d  37462  cdleme32f  37464  cdleme32le  37465  cdleme35h2  37475  cdleme38n  37482  cdleme40m  37485  cdleme41snaw  37494  cdleme42ke  37503  cdleme17d3  37514  cdleme48fvg  37518  cdlemeg46fvcl  37524  cdlemeg46fgN  37552  cdleme48gfv1  37554  cdleme48fgv  37556  cdleme50trn3  37571  trlord  37587  ltrniotavalbN  37602  cdlemb3  37624  cdlemg6c  37638  cdlemg6  37641  cdlemg7N  37644  cdlemg8c  37647  cdlemg8  37649  cdlemg11a  37655  cdlemg11b  37660  cdlemg12e  37665  cdlemg15a  37673  cdlemg15  37674  cdlemg16  37675  cdlemg16z  37677  cdlemg16zz  37678  cdlemg17dN  37681  cdlemg18a  37696  cdlemg20  37703  cdlemg22  37705  cdlemg24  37706  cdlemg37  37707  cdlemg31d  37718  cdlemg29  37723  cdlemg33b  37725  cdlemg33  37729  cdlemg38  37733  cdlemg39  37734  cdlemg40  37735  trlco  37745  trlcone  37746  cdlemg42  37747  cdlemg44b  37750  ltrncom  37756  trljco  37758  tendococl  37790  tendoplcl  37799  tendoplcom  37800  cdlemj2  37840  cdlemj3  37841  tendoid0  37843  tendoconid  37847  tendotr  37848  cdlemk25-3  37922  cdlemk26b-3  37923  cdlemk34  37928  cdlemk36  37931  cdlemk38  37933  cdlemkid4  37952  cdlemk35s-id  37956  cdlemk39s-id  37958  cdlemk19x  37961  cdlemk53  37975  cdlemk55  37979  cdlemk55u  37984  cdlemk39u  37986  cdlemk19u  37988  cdlemk56  37989  tendoex  37993  cdleml3N  37996  cdleml5N  37998  tendospcanN  38041  cdlemm10N  38136  cdlemn11pre  38228  dihord2pre  38243  dihvalcqpre  38253  dihopelvalcpre  38266  dihord6apre  38274  dihord5b  38277  dihord5apre  38280  dihord  38282  dihmeetlem1N  38308  dihglblem5apreN  38309  dihglblem3N  38313  dihmeetlem2N  38317  dihglbcpreN  38318  dihmeetbN  38321  dihmeetlem4preN  38324  dihmeetlem5  38326  dihmeetlem7N  38328  dihmeetlem10N  38334  dihmeetlem11N  38335  dihmeetlem12N  38336  dihmeetlem13N  38337  dihmeetlem15N  38339  dihmeetlem16N  38340  dihmeetlem17N  38341  dihmeetlem18N  38342  dihmeetlem19N  38343  dihmeetALTN  38345  dih1dimatlem0  38346  dihlspsnssN  38350  dihlspsnat  38351  mapdh8ad  38797  hdmap14lem14  38899  hgmapvvlem3  38943  resubcan2  39098  mzprename  39226  eldioph2lem1  39237  lzunuz  39245  rencldnfi  39298  pellexlem2  39307  infmrgelbi  39355  pellfundglb  39362  pellfund14gap  39364  qirropth  39385  rmxycomplete  39394  congadd  39443  acongeq  39460  jm2.19  39470  jm2.23  39473  jm2.20nn  39474  jm2.27  39485  jm3.1  39497  aomclem6  39539  lnmepi  39565  lmhmfgsplit  39566  lmhmlnmsplit  39567  pwssplit4  39569  hbtlem2  39604  hbtlem5  39608  dgraa0p  39629  proot1hash  39680  iocunico  39697  relexpxpmin  39942  brtrclfv2  39952  ntrclsiso  40297  ntrclskb  40299  ntrclsk3  40300  k0004lem3  40379  grur1cld  40448  ismnu  40477  grumnudlem  40501  suprnmpt  41310  wessf1ornlem  41325  projf1o  41339  snunioo1  41668  iccintsng  41679  lptre2pt  41801  limcleqr  41805  fnlimfvre  41835  limsupgtlem  41938  volioc  42137  iblspltprt  42138  stoweidlem19  42185  stoweidlem20  42186  stoweidlem22  42188  stoweidlem28  42194  stoweidlem34  42200  stoweidlem44  42210  stoweidlem60  42226  wallispilem3  42233  fourierdlem41  42314  fourierdlem42  42315  fourierdlem49  42321  fourierdlem51  42323  fourierdlem54  42326  fourierdlem74  42346  fourierdlem97  42369  caratheodorylem2  42690  ovnsubaddlem2  42734  hspmbllem2  42790  smflimmpt  42965  smflimsupmpt  42984  smfliminfmpt  42987  fzopredsuc  43404  fzoopth  43408  iccpartigtl  43430  lighneal  43623  oexpnegALTV  43689  oexpnegnz  43690  tgblthelfgott  43827  submefmnd  43962  lidldomn1  44090  ofaddmndmap  44290  lincdifsn  44377  lincellss  44379  lincresunit3lem3  44427  islindeps2  44436  lindssnlvec  44439  fdivmptf  44499  refdivmptf  44500  rrx2linest  44627  itsclc0yqsollem1  44647  itsclc0b  44657  itsclquadb  44661  itscnhlinecirc02plem3  44669
  Copyright terms: Public domain W3C validator