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

Theorem simpl1 1188
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 486 . 2 ((𝜑𝜃) → 𝜑)
213ad2antl1 1182 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:  simpl11  1245  simpl21  1248  simpl31  1251  simp1l1  1263  simp2l1  1269  simp3l1  1275  3anandirs  1469  rspc3ev  3623  2nreu  4376  f1prex  7032  cocan1  7039  weniso  7100  smogt  8000  smorndom  8001  omeulem1  8204  nnmord  8254  nnmword  8255  difsnen  8595  enfixsn  8622  mapunen  8683  ac6sfi  8759  fipreima  8827  elfiun  8891  ordiso2  8976  wemaplem2  9008  wemapso  9012  en2eqpr  9431  indcardi  9465  fodomfi2  9484  iunfictbso  9538  infmap2  9638  cofsmo  9689  cfsmolem  9690  coftr  9693  fin23lem11  9737  fincssdom  9743  fin23lem26  9745  isf32lem9  9781  ac6num  9899  gchdomtri  10049  gchpwdom  10090  winainflem  10113  tskuni  10203  gruima  10222  gruf  10231  grudomon  10237  elnpi  10408  distrlem4pr  10446  prlem934  10453  addcan  10822  addcan2  10823  divmulass  11319  divmulasscom  11320  ltmul1a  11487  suprleub  11603  supmul1  11606  suprzcl  12059  uzsupss  12337  xleadd1a  12643  xlesubadd  12653  xmulasslem3  12676  xlemul2a  12679  xadddilem  12684  xadddi2  12687  ixxun  12751  icoshftf1o  12861  ioounsn  12864  snunioc  12867  lincmb01cmp  12882  iccf1o  12883  nn0p1elfzo  13084  fzofzim  13088  ltexp2a  13535  leexp2  13540  ltexp2r  13542  exple1  13545  expnlbnd2  13600  fun2dmnop0  13857  ccatass  13942  ccat2s1fvwOLD  13999  swrdswrdlem  14066  ccatopth  14078  repswpfx  14147  2cshw  14175  cshimadifsn  14191  cshimadifsn0  14192  cshco  14198  repsco  14202  s2f1o  14278  limsupgre  14838  addcn2  14950  mulcn2  14952  ntrivcvgmul  15258  binomrisefac  15396  dvdsmodexp  15615  dvdsadd2b  15656  dvdsmod  15678  oexpneg  15694  sadass  15818  gcdass  15893  rplpwr  15905  rppwr  15906  lcmfunsnlem1  15979  coprmdvds2  15996  rpmulgcd2  15998  qredeq  15999  rpdvds  16002  cncongr2  16010  rpexp  16062  prmdiveq  16121  hashgcdlem  16123  odzdvds  16130  modprmn0modprm0  16142  coprimeprodsq2  16144  pythagtriplem3  16153  pcdvdsb  16203  pcgcd1  16211  qexpz  16235  pockthg  16240  vdwnnlem1  16329  0ram  16354  ramz2  16358  lubss  17731  lubun  17733  clatleglb  17736  clatglbss  17737  mrelatglb  17794  isnsgrp  17905  issubmnd  17938  ress0g  17939  gsumccatOLD  18005  gsumccat  18006  frmdss2  18028  submefmnd  18060  mulgneg  18246  mulgdirlem  18258  submmulg  18271  subgmulg  18293  nmzsubg  18317  ghmmulg  18370  gsmsymgreqlem1  18558  pmtrfb  18593  psgnunilem4  18625  odmodnn0  18668  odnncl  18673  odmod  18674  odmulgid  18681  odmulgeq  18684  odf1o1  18697  odf1o2  18698  odngen  18702  gexdvdsi  18708  pgpfi1  18720  odcau  18729  subgslw  18741  fislw  18750  lsmssv  18768  lsmless1x  18769  lsmless2x  18770  lsmsubm  18778  lsmmod  18801  lsmmod2  18802  efgred  18874  cntzcmn  18960  ghmplusg  18966  odadd1  18968  odadd2  18969  odadd  18970  lsmcomx  18976  gsumconst  19054  ablsimpgprmd  19237  srg1zr  19279  ring1eq0  19343  mulgass2  19354  isabvd  19591  rmodislmodlem  19701  rmodislmod  19702  lssintcl  19736  0lmhm  19812  lmhmvsca  19817  reslmhm2b  19826  pwssplit1  19831  pwssplit3  19833  lspfixed  19900  lspsnat  19917  lidldvgen  20028  issubassa  20098  evlsval2  20300  psrplusgpropd  20404  coe1subfv  20434  coe1mul2  20437  xrsdsreclblem  20591  regsumsupp  20766  obselocv  20872  uvcresum  20937  frlmsslsp  20940  frlmup4  20945  lindff1  20964  f1lindf  20966  lsslindf  20974  islindf4  20982  lbslcic  20985  mhmvlin  21008  mpomatmul  21055  mamutpos  21067  scmatscmide  21116  mavmulsolcl  21160  marrepcl  21173  mdetdiag  21208  mdetunilem1  21221  mdetunilem3  21223  mdetunilem7  21227  mdetunilem9  21229  mdetmul  21232  slesolinvbi  21290  m2pmfzmap  21355  pmatcollpwlem  21388  pmatcollpw  21389  mp2pm2mplem4  21417  chpdmatlem3  21448  chfacfisfcpmat  21463  chfacfscmulgsum  21468  chfacfpmmulgsum  21472  chfacfpmmulgsum2  21473  cayhamlem1  21474  cpmidpmatlem2  21479  cpmadugsumlemB  21482  cpmadugsumlemC  21483  cpmadugsumlemF  21484  riinopn  21516  neiint  21712  topssnei  21732  restntr  21790  iscnp4  21871  cnconst2  21891  cnrest2  21894  cnprest2  21898  cnpdis  21901  cnt0  21954  cnt1  21958  cnhaus  21962  ordthauslem  21991  cncmp  22000  fiuncmp  22012  sscmp  22013  hauscmp  22015  cnconn  22030  unconn  22037  nlly2i  22084  llynlly  22085  nllyidm  22097  finlocfin  22128  ptrescn  22247  xkococnlem  22267  qtopss  22323  kqfvima  22338  r0cld  22346  ordthmeolem  22409  fbssint  22446  fmf  22553  fmss  22554  elfm  22555  rnelfmlem  22560  rnelfm  22561  fmco  22569  flimss2  22580  flimss1  22581  flimrest  22591  flftg  22604  cnpflf2  22608  cnpflf  22609  flfcnp  22612  supnfcls  22628  fclsss1  22630  fclsss2  22631  fcfnei  22643  fcfelbas  22644  cnpfcfi  22648  subgntr  22715  opnsubg  22716  cldsubg  22719  ghmcnp  22723  utop2nei  22859  neipcfilu  22905  bldisj  23008  blgt0  23009  bl2in  23010  blss2ps  23013  blss2  23014  blssps  23034  blss  23035  xmetresbl  23047  lpbl  23113  blcld  23115  stdbdbl  23127  metcnp3  23150  metcnp2  23152  txmetcnp  23157  blval2  23172  nmoix  23338  nmoeq0  23345  icoopnst  23547  iocopnst  23548  xrhmeo  23554  nmhmcn  23728  cphsqrtcl2  23794  cphsqrtcl3  23795  cfil3i  23876  caublcls  23916  bcthlem5  23935  cmetcusp1  23960  cssbn  23982  rrxcph  23999  pjth  24046  ovoliunlem2  24110  volun  24152  volsup2  24212  mbfimaopn2  24264  iblconst  24424  itgconst  24425  dvcnp2  24526  dvcn  24527  deg1mul3le  24720  deg1tmle  24721  dvdsq1p  24764  ig1peu  24775  ig1pdvds  24780  coeid3  24840  dgrmulc  24871  efcvx  25047  tanord  25133  logdivlti  25214  logccv  25257  recxpcl  25269  cxpeq  25349  ang180  25403  isosctrlem2  25408  cxp2lim  25565  amgm  25579  muval1  25721  dvdssqf  25726  mumullem2  25768  mumul  25769  bcmono  25864  lgsfcl2  25890  lgsdilem  25911  lgsdirprm  25918  lgsdir  25919  lgsdi  25921  lgsne0  25922  padicabv  26217  brbtwn2  26702  colinearalglem1  26703  colinearalg  26707  axcgrtr  26712  axsegconlem8  26721  axsegconlem9  26722  axsegconlem10  26723  axcontlem8  26768  axcontlem10  26770  elntg2  26782  vtxdlfuhgr1v  27272  umgr2wlk  27738  erclwwlksym  27809  clwwlkfo  27838  clwwlkext2edg  27844  erclwwlknsym  27858  clwwlknon1  27885  numclwwlk2lem1  28164  numclwwlk5  28176  frgrregord13  28184  nvmul0or  28436  ipval2lem2  28490  lnomul  28546  shless  29145  shlej1  29146  pjspansn  29363  hoadddi  29589  kbmul  29741  homco2  29763  kbass2  29903  eliccelico  30511  elicoelioo  30512  iocinioc2  30513  iocinif  30515  swrdrn2  30639  xrge0adddir  30711  xrge0npcan  30713  archiabl  30859  ress1r  30893  rhmdvdsr  30924  pidlnz  30973  ssmxidl  31020  pstmfval  31196  fmcncfil  31231  zrhnm  31267  qqhnm  31288  measvunilem  31528  volfiniune  31546  dya2iocnrect  31596  sibfinima  31654  probun  31734  probinc  31736  cndprob01  31750  signstfvp  31898  bnj517  32214  bnj594  32241  pconnpi1  32541  cvmsss2  32578  mrsubcv  32814  msubvrs  32864  dvdspw  33039  br6  33050  br4  33051  frpomin  33135  frrlem4  33183  frrlem10  33189  fprlem1  33194  nosep1o  33243  nosepssdm  33247  nolt02olem  33255  nosupres  33264  nosupbnd1lem1  33265  nosupbnd1lem4  33268  nosupbnd1lem5  33269  nosupbnd1lem6  33270  nosupbnd2  33273  noetalem2  33275  cgrcomim  33507  cgrtriv  33520  cgrextend  33526  segconeq  33528  btwntriv2  33530  btwnintr  33537  btwnexch3  33538  btwnouttr2  33540  trisegint  33546  cgrsub  33563  cgrxfr  33573  btwnxfr  33574  lineext  33594  btwnconn1lem13  33617  btwnconn1lem14  33618  btwnconn3  33621  segcon2  33623  brsegle  33626  brsegle2  33627  segletr  33632  segleantisym  33633  seglelin  33634  outsideofeu  33649  lineunray  33665  lineelsb2  33666  ivthALT  33740  lindsenlbs  34997  areacirc  35095  cocanfo  35101  upixp  35112  ismtyima  35186  rrndstprj2  35214  zerdivemp1x  35330  lsatfixedN  36250  lssat  36257  eqlkr  36340  eqlkr2  36341  lkrlsp  36343  lshpkrlem4  36354  opposet  36422  cvrcon3b  36518  cvrcmp  36524  atlen0  36551  atnle  36558  atlatmstc  36560  cvlatexch3  36579  cvlsupr2  36584  hlsupr2  36628  hlrelat2  36644  cvrexchlem  36660  lnnat  36668  atcvrj2b  36673  atle  36677  atexchcvrN  36681  atbtwn  36687  athgt  36697  3dimlem3  36702  3dim1  36708  1cvratlt  36715  1cvrjat  36716  ps-1  36718  ps-2  36719  3atlem3  36726  3atlem5  36728  3atlem7  36730  llni  36749  llni2  36753  atcvrlln2  36760  llnexatN  36762  llncmp  36763  2llnmat  36765  2at0mat0  36766  lplni  36773  lplnnle2at  36782  2atnelpln  36785  lplnllnneN  36797  llncvrlpln2  36798  2lplnmN  36800  2llnmj  36801  lplncmp  36803  lplnexatN  36804  lplnexllnN  36805  2llnm3N  36810  lvoli  36816  lvoli3  36818  islvol2aN  36833  4atlem0a  36834  4atlem3  36837  4atlem3a  36838  4atlem4a  36840  4atlem4b  36841  4atlem4c  36842  4atlem4d  36843  4atlem10b  36846  4atlem11  36850  4atlem12  36853  lplncvrlvol2  36856  lvolcmp  36858  2lplnmj  36863  islinei  36981  pmapglbx  37010  linepmap  37016  lneq2at  37019  lnjatN  37021  lncvrat  37023  lncmp  37024  2llnma3r  37029  elpaddatriN  37044  elpaddat  37045  paddcom  37054  paddss1  37058  paddss2  37059  paddss12  37060  paddasslem6  37066  paddasslem7  37067  paddasslem8  37068  paddasslem9  37069  paddasslem15  37075  pmodlem2  37088  pmodl42N  37092  pmapjoin  37093  llnmod1i2  37101  2polcon4bN  37159  polcon2bN  37161  poml4N  37194  poml6N  37196  osumcllem1N  37197  osumcllem2N  37198  osumcllem11N  37207  osumclN  37208  pmapojoinN  37209  pexmidlem2N  37212  pexmidlem3N  37213  pexmidlem4N  37214  pexmidlem6N  37216  pexmidlem7N  37217  pl42lem2N  37221  pl42lem3N  37222  pl42lem4N  37223  pl42N  37224  lhpexle2lem  37250  lhpexle3lem  37252  lhpexle3  37253  lhpmcvr3  37266  lhp2at0nle  37276  lhprelat3N  37281  4atex  37317  4atex2  37318  lauteq  37336  lautco  37338  ltrncoidN  37369  ltrneq2  37389  ltrnnidn  37415  ltrnideq  37416  trlnid  37420  ltrnatlw  37424  trlnle  37427  trlval3  37428  trlval4  37429  cdlemc  37438  cdlemd5  37443  cdlemd9  37447  ltrneq3  37449  cdleme0moN  37466  cdleme20  37565  cdleme21j  37577  cdleme21  37578  cdleme27cl  37607  cdlemefrs29bpre0  37637  cdlemefs27cl  37654  cdlemefs32sn1aw  37655  cdleme43fsv1snlem  37661  cdleme32d  37685  cdleme32f  37687  cdleme32le  37688  cdleme35h2  37698  cdleme38n  37705  cdleme40m  37708  cdleme41snaw  37717  cdleme42ke  37726  cdleme17d3  37737  cdleme48fvg  37741  cdlemeg46fvcl  37747  cdlemeg46fgN  37775  cdleme48gfv1  37777  cdleme48fgv  37779  cdleme50trn3  37794  trlord  37810  ltrniotavalbN  37825  cdlemb3  37847  cdlemg6c  37861  cdlemg6  37864  cdlemg7N  37867  cdlemg8c  37870  cdlemg8  37872  cdlemg11a  37878  cdlemg11b  37883  cdlemg12e  37888  cdlemg15a  37896  cdlemg15  37897  cdlemg16  37898  cdlemg16z  37900  cdlemg16zz  37901  cdlemg17dN  37904  cdlemg18a  37919  cdlemg20  37926  cdlemg22  37928  cdlemg24  37929  cdlemg37  37930  cdlemg31d  37941  cdlemg29  37946  cdlemg33b  37948  cdlemg33  37952  cdlemg38  37956  cdlemg39  37957  cdlemg40  37958  trlco  37968  trlcone  37969  cdlemg42  37970  cdlemg44b  37973  ltrncom  37979  trljco  37981  tendococl  38013  tendoplcl  38022  tendoplcom  38023  cdlemj2  38063  cdlemj3  38064  tendoid0  38066  tendoconid  38070  tendotr  38071  cdlemk25-3  38145  cdlemk26b-3  38146  cdlemk34  38151  cdlemk36  38154  cdlemk38  38156  cdlemkid4  38175  cdlemk35s-id  38179  cdlemk39s-id  38181  cdlemk19x  38184  cdlemk53  38198  cdlemk55  38202  cdlemk55u  38207  cdlemk39u  38209  cdlemk19u  38211  cdlemk56  38212  tendoex  38216  cdleml3N  38219  cdleml5N  38221  tendospcanN  38264  cdlemm10N  38359  cdlemn11pre  38451  dihord2pre  38466  dihvalcqpre  38476  dihopelvalcpre  38489  dihord6apre  38497  dihord5b  38500  dihord5apre  38503  dihord  38505  dihmeetlem1N  38531  dihglblem5apreN  38532  dihglblem3N  38536  dihmeetlem2N  38540  dihglbcpreN  38541  dihmeetbN  38544  dihmeetlem4preN  38547  dihmeetlem5  38549  dihmeetlem7N  38551  dihmeetlem10N  38557  dihmeetlem11N  38558  dihmeetlem12N  38559  dihmeetlem13N  38560  dihmeetlem15N  38562  dihmeetlem16N  38563  dihmeetlem17N  38564  dihmeetlem18N  38565  dihmeetlem19N  38566  dihmeetALTN  38568  dih1dimatlem0  38569  dihlspsnssN  38573  dihlspsnat  38574  mapdh8ad  39020  hdmap14lem14  39122  hgmapvvlem3  39166  resubcan2  39456  mzprename  39606  eldioph2lem1  39617  lzunuz  39625  rencldnfi  39678  pellexlem2  39687  infmrgelbi  39735  pellfundglb  39742  pellfund14gap  39744  qirropth  39765  rmxycomplete  39774  congadd  39823  acongeq  39840  jm2.19  39850  jm2.23  39853  jm2.20nn  39854  jm2.27  39865  jm3.1  39877  aomclem6  39919  lnmepi  39945  lmhmfgsplit  39946  lmhmlnmsplit  39947  pwssplit4  39949  hbtlem2  39984  hbtlem5  39988  dgraa0p  40009  proot1hash  40060  iocunico  40077  relexpxpmin  40334  brtrclfv2  40344  ntrclsiso  40689  ntrclskb  40691  ntrclsk3  40692  k0004lem3  40771  grur1cld  40860  ismnu  40889  grumnudlem  40913  suprnmpt  41721  wessf1ornlem  41736  projf1o  41750  snunioo1  42075  iccintsng  42086  lptre2pt  42208  limcleqr  42212  fnlimfvre  42242  limsupgtlem  42345  volioc  42540  iblspltprt  42541  stoweidlem19  42587  stoweidlem20  42588  stoweidlem22  42590  stoweidlem28  42596  stoweidlem34  42602  stoweidlem44  42612  stoweidlem60  42628  wallispilem3  42635  fourierdlem41  42716  fourierdlem42  42717  fourierdlem49  42723  fourierdlem51  42725  fourierdlem54  42728  fourierdlem74  42748  fourierdlem97  42771  caratheodorylem2  43092  ovnsubaddlem2  43136  hspmbllem2  43192  smflimmpt  43367  smflimsupmpt  43386  smfliminfmpt  43389  fzopredsuc  43806  fzoopth  43810  imasetpreimafvbijlemfv  43845  iccpartigtl  43866  lighneal  44055  oexpnegALTV  44121  oexpnegnz  44122  tgblthelfgott  44259  lidldomn1  44471  ofaddmndmap  44671  lincdifsn  44759  lincellss  44761  lincresunit3lem3  44809  islindeps2  44818  lindssnlvec  44821  fdivmptf  44881  refdivmptf  44882  rrx2linest  45082  itsclc0yqsollem1  45102  itsclc0b  45112  itsclquadb  45116  itscnhlinecirc02plem3  45124
  Copyright terms: Public domain W3C validator