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

Theorem simpl1 1193
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 1187 1 (((𝜑𝜓𝜒) ∧ 𝜃) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  w3a 1089
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 1091
This theorem is referenced by:  simpl11  1250  simpl21  1253  simpl31  1256  simp1l1  1268  simp2l1  1274  simp3l1  1280  3anandirs  1474  rspc3ev  3563  2nreu  4370  predtrss  6197  frpomin  6211  f1prex  7112  cocan1  7119  weniso  7181  frrlem4  8050  frrlem10  8056  fprlem1  8061  smogt  8124  smorndom  8125  omeulem1  8330  nnmord  8380  nnmword  8381  difsnen  8749  enfixsn  8776  mapunen  8837  ac6sfi  8939  fipreima  9006  elfiun  9070  ordiso2  9155  wemaplem2  9187  en2eqpr  9645  indcardi  9679  fodomfi2  9698  iunfictbso  9752  infmap2  9856  cofsmo  9907  cfsmolem  9908  coftr  9911  fin23lem11  9955  fincssdom  9961  fin23lem26  9963  isf32lem9  9999  ac6num  10117  gchdomtri  10267  gchpwdom  10308  winainflem  10331  tskuni  10421  gruima  10440  gruf  10449  grudomon  10455  elnpi  10626  distrlem4pr  10664  prlem934  10671  addcan  11040  addcan2  11041  divmulass  11537  divmulasscom  11538  ltmul1a  11705  suprleub  11822  supmul1  11825  suprzcl  12281  uzsupss  12560  xleadd1a  12867  xlesubadd  12877  xmulasslem3  12900  xlemul2a  12903  xadddilem  12908  xadddi2  12911  ixxun  12975  icoshftf1o  13086  ioounsn  13089  snunioc  13092  lincmb01cmp  13107  iccf1o  13108  nn0p1elfzo  13309  fzofzim  13313  ltexp2a  13760  leexp2  13765  ltexp2r  13767  exple1  13770  expnlbnd2  13825  fun2dmnop0  14084  ccatass  14169  ccat2s1fvwOLD  14226  swrdswrdlem  14293  ccatopth  14305  repswpfx  14374  2cshw  14402  cshimadifsn  14418  cshimadifsn0  14419  cshco  14425  repsco  14429  s2f1o  14505  limsupgre  15066  addcn2  15179  mulcn2  15181  ntrivcvgmul  15490  binomrisefac  15628  dvdsmodexp  15847  dvdsadd2b  15891  dvdsexp2im  15912  dvdsmod  15914  oexpneg  15930  sadass  16054  gcdass  16131  rplpwr  16143  lcmfunsnlem1  16218  coprmdvds2  16235  rpmulgcd2  16237  qredeq  16238  rpdvds  16241  cncongr2  16249  rpexp  16303  prmdiveq  16363  hashgcdlem  16365  odzdvds  16372  modprmn0modprm0  16384  coprimeprodsq2  16386  pythagtriplem3  16395  pcdvdsb  16446  pcgcd1  16454  qexpz  16478  pockthg  16483  vdwnnlem1  16572  0ram  16597  ramz2  16601  lubss  18043  lubun  18045  clatleglb  18048  clatglbss  18049  mrelatglb  18090  isnsgrp  18191  issubmnd  18224  ress0g  18225  gsumccatOLD  18291  gsumccat  18292  frmdss2  18314  submefmnd  18346  mulgneg  18534  mulgdirlem  18546  submmulg  18559  subgmulg  18581  nmzsubg  18605  ghmmulg  18658  gsmsymgreqlem1  18846  pmtrfb  18881  psgnunilem4  18913  odmodnn0  18956  odnncl  18961  odmod  18962  odmulgid  18969  odmulgeq  18972  odf1o1  18985  odf1o2  18986  odngen  18990  gexdvdsi  18996  pgpfi1  19008  odcau  19017  subgslw  19029  fislw  19038  lsmssv  19056  lsmless1x  19057  lsmless2x  19058  lsmsubm  19066  lsmmod  19089  lsmmod2  19090  efgred  19162  cntzcmn  19249  ghmplusg  19255  odadd1  19257  odadd2  19258  odadd  19259  lsmcomx  19265  gsumconst  19343  ablsimpgprmd  19526  srg1zr  19568  ring1eq0  19632  mulgass2  19643  isabvd  19880  rmodislmodlem  19990  rmodislmod  19991  lssintcl  20025  0lmhm  20101  lmhmvsca  20106  reslmhm2b  20115  pwssplit1  20120  pwssplit3  20122  lspfixed  20189  lspsnat  20206  lidldvgen  20317  xrsdsreclblem  20433  regsumsupp  20608  obselocv  20714  uvcresum  20779  frlmsslsp  20782  frlmup4  20787  lindff1  20806  f1lindf  20808  lsslindf  20816  islindf4  20824  lbslcic  20827  issubassa  20852  evlsval2  21071  psrplusgpropd  21181  coe1subfv  21211  coe1mul2  21214  mhmvlin  21320  mpomatmul  21367  mamutpos  21379  scmatscmide  21428  mavmulsolcl  21472  marrepcl  21485  mdetdiag  21520  mdetunilem1  21533  mdetunilem3  21535  mdetunilem7  21539  mdetunilem9  21541  mdetmul  21544  slesolinvbi  21602  m2pmfzmap  21668  pmatcollpwlem  21701  pmatcollpw  21702  mp2pm2mplem4  21730  chpdmatlem3  21761  chfacfisfcpmat  21776  chfacfscmulgsum  21781  chfacfpmmulgsum  21785  chfacfpmmulgsum2  21786  cayhamlem1  21787  cpmidpmatlem2  21792  cpmadugsumlemB  21795  cpmadugsumlemC  21796  cpmadugsumlemF  21797  riinopn  21829  neiint  22025  topssnei  22045  restntr  22103  iscnp4  22184  cnconst2  22204  cnrest2  22207  cnprest2  22211  cnpdis  22214  cnt0  22267  cnt1  22271  cnhaus  22275  ordthauslem  22304  cncmp  22313  fiuncmp  22325  sscmp  22326  hauscmp  22328  cnconn  22343  unconn  22350  nlly2i  22397  llynlly  22398  nllyidm  22410  finlocfin  22441  ptrescn  22560  xkococnlem  22580  qtopss  22636  kqfvima  22651  r0cld  22659  ordthmeolem  22722  fbssint  22759  fmf  22866  fmss  22867  elfm  22868  rnelfmlem  22873  rnelfm  22874  fmco  22882  flimss2  22893  flimss1  22894  flimrest  22904  flftg  22917  cnpflf2  22921  cnpflf  22922  flfcnp  22925  supnfcls  22941  fclsss1  22943  fclsss2  22944  fcfnei  22956  fcfelbas  22957  cnpfcfi  22961  subgntr  23028  opnsubg  23029  cldsubg  23032  ghmcnp  23036  utop2nei  23172  neipcfilu  23217  bldisj  23320  blgt0  23321  bl2in  23322  blss2ps  23325  blss2  23326  blssps  23346  blss  23347  xmetresbl  23359  lpbl  23425  blcld  23427  stdbdbl  23439  metcnp3  23462  metcnp2  23464  txmetcnp  23469  blval2  23484  nmoix  23651  nmoeq0  23658  icoopnst  23860  iocopnst  23861  xrhmeo  23867  nmhmcn  24041  cphsqrtcl2  24107  cphsqrtcl3  24108  cfil3i  24190  caublcls  24230  bcthlem5  24249  cmetcusp1  24274  cssbn  24296  rrxcph  24313  pjth  24360  ovoliunlem2  24424  volun  24466  volsup2  24526  mbfimaopn2  24578  iblconst  24739  itgconst  24740  dvcnp2  24841  dvcn  24842  deg1mul3le  25038  deg1tmle  25039  dvdsq1p  25082  ig1peu  25093  ig1pdvds  25098  coeid3  25158  dgrmulc  25189  efcvx  25365  tanord  25451  logdivlti  25532  logccv  25575  recxpcl  25587  cxpeq  25667  ang180  25721  isosctrlem2  25726  cxp2lim  25883  amgm  25897  muval1  26039  dvdssqf  26044  mumullem2  26086  mumul  26087  bcmono  26182  lgsfcl2  26208  lgsdilem  26229  lgsdirprm  26236  lgsdir  26237  lgsdi  26239  lgsne0  26240  padicabv  26535  brbtwn2  27020  colinearalglem1  27021  colinearalg  27025  axcgrtr  27030  axsegconlem8  27039  axsegconlem9  27040  axsegconlem10  27041  axcontlem8  27086  axcontlem10  27088  elntg2  27100  vtxdlfuhgr1v  27591  umgr2wlk  28057  erclwwlksym  28128  clwwlkfo  28157  clwwlkext2edg  28163  erclwwlknsym  28177  clwwlknon1  28204  numclwwlk2lem1  28483  numclwwlk5  28495  frgrregord13  28503  nvmul0or  28755  ipval2lem2  28809  lnomul  28865  shless  29464  shlej1  29465  pjspansn  29682  hoadddi  29908  kbmul  30060  homco2  30082  kbass2  30222  eliccelico  30842  elicoelioo  30843  iocinioc2  30844  iocinif  30846  swrdrn2  30970  xrge0adddir  31044  xrge0npcan  31046  archiabl  31195  ress1r  31229  rhmdvdsr  31260  pidlnz  31309  grplsm0l  31329  intlidl  31340  ssmxidl  31380  pstmfval  31584  fmcncfil  31619  zrhnm  31655  qqhnm  31676  measvunilem  31916  volfiniune  31934  dya2iocnrect  31984  sibfinima  32042  probun  32122  probinc  32124  cndprob01  32138  signstfvp  32286  bnj517  32601  bnj594  32628  pconnpi1  32935  cvmsss2  32972  mrsubcv  33208  msubvrs  33258  br6  33466  br4  33467  nosep1o  33647  nosep2o  33648  nosepssdm  33652  nolt02olem  33660  nosupres  33673  nosupbnd1lem1  33674  nosupbnd1lem4  33677  nosupbnd1lem5  33678  nosupbnd1lem6  33679  nosupbnd2  33682  noinfres  33688  noinfbnd1lem1  33689  noinfbnd1lem4  33692  noinfbnd1lem6  33694  noinfbnd2  33697  noetasuplem3  33701  noetalem1  33707  scutbdaybnd  33772  sltlpss  33850  coinitsslt  33852  cgrcomim  34054  cgrtriv  34067  cgrextend  34073  segconeq  34075  btwntriv2  34077  btwnintr  34084  btwnexch3  34085  btwnouttr2  34087  trisegint  34093  cgrsub  34110  cgrxfr  34120  btwnxfr  34121  lineext  34141  btwnconn1lem13  34164  btwnconn1lem14  34165  btwnconn3  34168  segcon2  34170  brsegle  34173  brsegle2  34174  segletr  34179  segleantisym  34180  seglelin  34181  outsideofeu  34196  lineunray  34212  lineelsb2  34213  ivthALT  34287  lindsenlbs  35535  areacirc  35633  cocanfo  35639  upixp  35650  ismtyima  35724  rrndstprj2  35752  zerdivemp1x  35868  lsatfixedN  36786  lssat  36793  eqlkr  36876  eqlkr2  36877  lkrlsp  36879  lshpkrlem4  36890  opposet  36958  cvrcon3b  37054  cvrcmp  37060  atlen0  37087  atnle  37094  atlatmstc  37096  cvlatexch3  37115  cvlsupr2  37120  hlsupr2  37164  hlrelat2  37180  cvrexchlem  37196  lnnat  37204  atcvrj2b  37209  atle  37213  atexchcvrN  37217  atbtwn  37223  athgt  37233  3dimlem3  37238  3dim1  37244  1cvratlt  37251  1cvrjat  37252  ps-1  37254  ps-2  37255  3atlem3  37262  3atlem5  37264  3atlem7  37266  llni  37285  llni2  37289  atcvrlln2  37296  llnexatN  37298  llncmp  37299  2llnmat  37301  2at0mat0  37302  lplni  37309  lplnnle2at  37318  2atnelpln  37321  lplnllnneN  37333  llncvrlpln2  37334  2lplnmN  37336  2llnmj  37337  lplncmp  37339  lplnexatN  37340  lplnexllnN  37341  2llnm3N  37346  lvoli  37352  lvoli3  37354  islvol2aN  37369  4atlem0a  37370  4atlem3  37373  4atlem3a  37374  4atlem4a  37376  4atlem4b  37377  4atlem4c  37378  4atlem4d  37379  4atlem10b  37382  4atlem11  37386  4atlem12  37389  lplncvrlvol2  37392  lvolcmp  37394  2lplnmj  37399  islinei  37517  pmapglbx  37546  linepmap  37552  lneq2at  37555  lnjatN  37557  lncvrat  37559  lncmp  37560  2llnma3r  37565  elpaddatriN  37580  elpaddat  37581  paddcom  37590  paddss1  37594  paddss2  37595  paddss12  37596  paddasslem6  37602  paddasslem7  37603  paddasslem8  37604  paddasslem9  37605  paddasslem15  37611  pmodlem2  37624  pmodl42N  37628  pmapjoin  37629  llnmod1i2  37637  2polcon4bN  37695  polcon2bN  37697  poml4N  37730  poml6N  37732  osumcllem1N  37733  osumcllem2N  37734  osumcllem11N  37743  osumclN  37744  pmapojoinN  37745  pexmidlem2N  37748  pexmidlem3N  37749  pexmidlem4N  37750  pexmidlem6N  37752  pexmidlem7N  37753  pl42lem2N  37757  pl42lem3N  37758  pl42lem4N  37759  pl42N  37760  lhpexle2lem  37786  lhpexle3lem  37788  lhpexle3  37789  lhpmcvr3  37802  lhp2at0nle  37812  lhprelat3N  37817  4atex  37853  4atex2  37854  lauteq  37872  lautco  37874  ltrncoidN  37905  ltrneq2  37925  ltrnnidn  37951  ltrnideq  37952  trlnid  37956  ltrnatlw  37960  trlnle  37963  trlval3  37964  trlval4  37965  cdlemc  37974  cdlemd5  37979  cdlemd9  37983  ltrneq3  37985  cdleme0moN  38002  cdleme20  38101  cdleme21j  38113  cdleme21  38114  cdleme27cl  38143  cdlemefrs29bpre0  38173  cdlemefs27cl  38190  cdlemefs32sn1aw  38191  cdleme43fsv1snlem  38197  cdleme32d  38221  cdleme32f  38223  cdleme32le  38224  cdleme35h2  38234  cdleme38n  38241  cdleme40m  38244  cdleme41snaw  38253  cdleme42ke  38262  cdleme17d3  38273  cdleme48fvg  38277  cdlemeg46fvcl  38283  cdlemeg46fgN  38311  cdleme48gfv1  38313  cdleme48fgv  38315  cdleme50trn3  38330  trlord  38346  ltrniotavalbN  38361  cdlemb3  38383  cdlemg6c  38397  cdlemg6  38400  cdlemg7N  38403  cdlemg8c  38406  cdlemg8  38408  cdlemg11a  38414  cdlemg11b  38419  cdlemg12e  38424  cdlemg15a  38432  cdlemg15  38433  cdlemg16  38434  cdlemg16z  38436  cdlemg16zz  38437  cdlemg17dN  38440  cdlemg18a  38455  cdlemg20  38462  cdlemg22  38464  cdlemg24  38465  cdlemg37  38466  cdlemg31d  38477  cdlemg29  38482  cdlemg33b  38484  cdlemg33  38488  cdlemg38  38492  cdlemg39  38493  cdlemg40  38494  trlco  38504  trlcone  38505  cdlemg42  38506  cdlemg44b  38509  ltrncom  38515  trljco  38517  tendococl  38549  tendoplcl  38558  tendoplcom  38559  cdlemj2  38599  cdlemj3  38600  tendoid0  38602  tendoconid  38606  tendotr  38607  cdlemk25-3  38681  cdlemk26b-3  38682  cdlemk34  38687  cdlemk36  38690  cdlemk38  38692  cdlemkid4  38711  cdlemk35s-id  38715  cdlemk39s-id  38717  cdlemk19x  38720  cdlemk53  38734  cdlemk55  38738  cdlemk55u  38743  cdlemk39u  38745  cdlemk19u  38747  cdlemk56  38748  tendoex  38752  cdleml3N  38755  cdleml5N  38757  tendospcanN  38800  cdlemm10N  38895  cdlemn11pre  38987  dihord2pre  39002  dihvalcqpre  39012  dihopelvalcpre  39025  dihord6apre  39033  dihord5b  39036  dihord5apre  39039  dihord  39041  dihmeetlem1N  39067  dihglblem5apreN  39068  dihglblem3N  39072  dihmeetlem2N  39076  dihglbcpreN  39077  dihmeetbN  39080  dihmeetlem4preN  39083  dihmeetlem5  39085  dihmeetlem7N  39087  dihmeetlem10N  39093  dihmeetlem11N  39094  dihmeetlem12N  39095  dihmeetlem13N  39096  dihmeetlem15N  39098  dihmeetlem16N  39099  dihmeetlem17N  39100  dihmeetlem18N  39101  dihmeetlem19N  39102  dihmeetALTN  39104  dih1dimatlem0  39105  dihlspsnssN  39109  dihlspsnat  39110  mapdh8ad  39556  hdmap14lem14  39658  hgmapvvlem3  39702  dvdsexpnn  40076  resubcan2  40107  mzprename  40302  eldioph2lem1  40313  lzunuz  40321  rencldnfi  40374  pellexlem2  40383  infmrgelbi  40431  pellfundglb  40438  pellfund14gap  40440  qirropth  40461  rmxycomplete  40470  congadd  40519  acongeq  40536  jm2.19  40546  jm2.23  40549  jm2.20nn  40550  jm2.27  40561  jm3.1  40573  aomclem6  40615  lnmepi  40641  lmhmfgsplit  40642  lmhmlnmsplit  40643  pwssplit4  40645  hbtlem2  40680  hbtlem5  40684  dgraa0p  40705  proot1hash  40756  iocunico  40773  relexpxpmin  41030  brtrclfv2  41040  ntrclsiso  41382  ntrclskb  41384  ntrclsk3  41385  k0004lem3  41464  grur1cld  41551  ismnu  41580  grumnudlem  41604  suprnmpt  42411  wessf1ornlem  42423  projf1o  42437  snunioo1  42753  iccintsng  42764  lptre2pt  42884  limcleqr  42888  fnlimfvre  42918  limsupgtlem  43021  volioc  43216  iblspltprt  43217  stoweidlem19  43263  stoweidlem20  43264  stoweidlem22  43266  stoweidlem28  43272  stoweidlem34  43278  stoweidlem44  43288  stoweidlem60  43304  wallispilem3  43311  fourierdlem41  43392  fourierdlem42  43393  fourierdlem49  43399  fourierdlem51  43401  fourierdlem54  43404  fourierdlem74  43424  fourierdlem97  43447  caratheodorylem2  43768  ovnsubaddlem2  43812  hspmbllem2  43868  smflimmpt  44043  smflimsupmpt  44062  smfliminfmpt  44065  funfocofob  44270  fzopredsuc  44516  fzoopth  44520  imasetpreimafvbijlemfv  44555  iccpartigtl  44576  lighneal  44764  oexpnegALTV  44830  oexpnegnz  44831  tgblthelfgott  44968  lidldomn1  45180  ofaddmndmap  45380  lincdifsn  45466  lincellss  45468  lincresunit3lem3  45516  islindeps2  45525  lindssnlvec  45528  fdivmptf  45588  refdivmptf  45589  rrx2linest  45789  itsclc0yqsollem1  45809  itsclc0b  45819  itsclquadb  45823  itscnhlinecirc02plem3  45831
  Copyright terms: Public domain W3C validator