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

Theorem simpl1 1235
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 470 . 2 ((𝜑𝜃) → 𝜑)
213ad2antl1 1229 1 (((𝜑𝜓𝜒) ∧ 𝜃) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1100
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 198  df-an 385  df-3an 1102
This theorem is referenced by:  simpll1OLD  1263  simprl1OLD  1275  simpl11  1322  simpl21  1328  simpl31  1334  simp1l1  1358  simp2l1  1364  simp3l1  1370  3anandirs  1589  rspc3ev  3519  f1prex  6763  cocan1  6770  weniso  6828  smogt  7700  smorndom  7701  omeulem1  7899  nnmord  7949  nnmword  7950  difsnen  8281  enfixsn  8308  mapunen  8368  ac6sfi  8443  fipreima  8511  elfiun  8575  ordiso2  8659  wemaplem2  8691  wemapso  8695  en2eqpr  9113  indcardi  9147  fodomfi2  9166  iunfictbso  9220  infmap2  9325  cofsmo  9376  cfsmolem  9377  coftr  9380  fin23lem11  9424  fincssdom  9430  fin23lem26  9432  isf32lem9  9468  ac6num  9586  gchdomtri  9736  gchpwdom  9777  winainflem  9800  tskuni  9890  gruima  9909  gruf  9918  grudomon  9924  elnpi  10095  distrlem4pr  10133  prlem934  10140  addcan  10505  addcan2  10506  divmulass  10993  divmulasscom  10994  ltmul1a  11157  suprleub  11274  supmul1  11277  suprzcl  11723  uzsupss  11999  xleadd1a  12301  xlesubadd  12311  xmulasslem3  12334  xlemul2a  12337  xadddilem  12342  xadddi2  12345  ixxun  12409  icoshftf1o  12516  ioounsn  12519  snunioc  12523  lincmb01cmp  12538  iccf1o  12539  nn0p1elfzo  12735  fzofzim  12739  ltexp2a  13135  leexp2  13138  ltexp2r  13140  exple1  13143  expnlbnd2  13218  fun2dmnop0  13493  ccatass  13585  ccat2s1fvw  13638  swrdswrdlem  13683  ccatopth  13694  cshimadifsn  13799  cshimadifsn0  13800  cshco  13806  repsco  13809  s2f1o  13885  limsupgre  14435  addcn2  14547  mulcn2  14549  ntrivcvgmul  14855  binomrisefac  14993  dvdsmodexp  15211  dvdsadd2b  15251  dvdsmod  15273  oexpneg  15289  sadass  15412  gcdass  15483  rplpwr  15495  rppwr  15496  lcmfunsnlem1  15569  coprmdvds2  15586  rpmulgcd2  15588  qredeq  15589  rpdvds  15592  cncongr2  15600  rpexp  15649  prmdiveq  15708  hashgcdlem  15710  odzdvds  15717  modprmn0modprm0  15729  coprimeprodsq2  15731  pythagtriplem3  15740  pcdvdsb  15790  pcgcd1  15798  qexpz  15822  pockthg  15827  vdwnnlem1  15916  0ram  15941  ramz2  15945  lubss  17326  lubun  17328  clatleglb  17331  clatglbss  17332  mrelatglb  17389  isnsgrp  17493  issubmnd  17523  ress0g  17524  gsumccat  17583  frmdss2  17605  mulgneg  17764  mulgdirlem  17775  submmulg  17788  subgmulg  17810  nmzsubg  17837  ghmmulg  17874  gsmsymgreqlem1  18051  pmtrfb  18086  psgnunilem4  18118  odmodnn0  18160  odnncl  18165  odmod  18166  odmulgid  18172  odmulgeq  18175  odf1o1  18188  odf1o2  18189  odngen  18193  gexdvdsi  18199  pgpfi1  18211  odcau  18220  subgslw  18232  fislw  18241  lsmssv  18259  lsmless1x  18260  lsmless2x  18261  lsmsubm  18269  lsmmod  18289  lsmmod2  18290  efgred  18362  cntzcmn  18446  ghmplusg  18450  odadd1  18452  odadd2  18453  odadd  18454  lsmcomx  18460  gsumconst  18535  srg1zr  18731  ring1eq0  18792  mulgass2  18803  isabvd  19024  rmodislmodlem  19134  rmodislmod  19135  lssintcl  19171  0lmhm  19247  lmhmvsca  19252  reslmhm2b  19261  pwssplit1  19266  pwssplit3  19268  lspfixed  19335  lspfixedOLD  19336  lspsnat  19353  lidldvgen  19464  issubassa  19533  evlsval2  19728  psrplusgpropd  19814  coe1subfv  19844  coe1mul2  19847  xrsdsreclblem  20000  regsumsupp  20177  obselocv  20282  uvcresum  20342  frlmsslsp  20345  frlmup4  20350  lindff1  20369  f1lindf  20371  lsslindf  20379  islindf4  20387  lbslcic  20390  mhmvlin  20413  mpt2matmul  20463  mamutpos  20475  scmatscmide  20524  mavmulsolcl  20568  marrepcl  20581  mdetdiag  20616  mdetunilem1  20629  mdetunilem3  20631  mdetunilem7  20635  mdetunilem9  20637  mdetmul  20640  slesolinvbi  20699  m2pmfzmap  20765  pmatcollpwlem  20798  pmatcollpw  20799  mp2pm2mplem4  20827  chpdmatlem3  20858  chfacfisfcpmat  20873  chfacfscmulgsum  20878  chfacfpmmulgsum  20882  chfacfpmmulgsum2  20883  cayhamlem1  20884  cpmidpmatlem2  20889  cpmadugsumlemB  20892  cpmadugsumlemC  20893  cpmadugsumlemF  20894  riinopn  20926  neiint  21122  topssnei  21142  restntr  21200  iscnp4  21281  cnconst2  21301  cnrest2  21304  cnprest2  21308  cnpdis  21311  cnt0  21364  cnt1  21368  cnhaus  21372  ordthauslem  21401  cncmp  21409  fiuncmp  21421  sscmp  21422  hauscmp  21424  cnconn  21439  unconn  21446  nlly2i  21493  llynlly  21494  nllyidm  21506  finlocfin  21537  ptrescn  21656  xkococnlem  21676  qtoptop2  21716  qtopss  21732  kqfvima  21747  r0cld  21755  ordthmeolem  21818  fbssint  21855  fmf  21962  fmss  21963  elfm  21964  rnelfmlem  21969  rnelfm  21970  fmco  21978  flimss2  21989  flimss1  21990  flimrest  22000  flftg  22013  cnpflf2  22017  cnpflf  22018  flfcnp  22021  supnfcls  22037  fclsss1  22039  fclsss2  22040  fcfnei  22052  fcfelbas  22053  cnpfcfi  22057  subgntr  22123  opnsubg  22124  cldsubg  22127  ghmcnp  22131  utop2nei  22267  neipcfilu  22313  bldisj  22416  blgt0  22417  bl2in  22418  blss2ps  22421  blss2  22422  blssps  22442  blss  22443  xmetresbl  22455  lpbl  22521  blcld  22523  stdbdbl  22535  metcnp3  22558  metcnp2  22560  txmetcnp  22565  blval2  22580  nmoix  22746  nmoeq0  22753  icoopnst  22951  iocopnst  22952  xrhmeo  22958  nmhmcn  23132  cphsqrtcl2  23198  cphsqrtcl3  23199  cfil3i  23279  caublcls  23319  bcthlem5  23337  cmetcusp1  23361  rrxcph  23392  pjth  23422  ovoliunlem2  23484  volun  23526  volsup2  23586  mbfimaopn2  23638  iblconst  23798  itgconst  23799  dvcnp2  23897  dvcn  23898  deg1mul3le  24090  deg1tmle  24091  dvdsq1p  24134  ig1peu  24145  ig1pdvds  24150  coeid3  24210  dgrmulc  24241  efcvx  24417  tanord  24499  logdivlti  24580  logccv  24623  recxpcl  24635  cxpeq  24712  ang180  24758  isosctrlem2  24763  cxp2lim  24917  amgm  24931  muval1  25073  dvdssqf  25078  mumullem2  25120  mumul  25121  bcmono  25216  lgsfcl2  25242  lgsdilem  25263  lgsdirprm  25270  lgsdir  25271  lgsdi  25273  lgsne0  25274  padicabv  25533  brbtwn2  25999  colinearalglem1  26000  colinearalg  26004  axcgrtr  26009  axsegconlem8  26018  axsegconlem9  26019  axsegconlem10  26020  axcontlem8  26065  axcontlem10  26067  vtxdlfuhgr1v  26603  umgr2wlk  27089  erclwwlksym  27164  clwwlkfo  27199  clwwlkext2edg  27206  erclwwlknsym  27221  clwlksf1clwwlklemOLD  27242  clwwlknon1  27265  numclwwlk2lem1  27556  numclwwlk2lem1OLD  27563  numclwwlk5  27576  frgrregord13  27584  nvmul0or  27833  ipval2lem2  27887  lnomul  27943  shless  28546  shlej1  28547  pjspansn  28764  hoadddi  28990  kbmul  29142  homco2  29164  kbass2  29304  eliccelico  29866  elicoelioo  29867  iocinioc2  29868  iocinif  29870  xrge0adddir  30017  xrge0npcan  30019  archiabl  30077  ress1r  30114  rhmdvdsr  30143  pstmfval  30264  fmcncfil  30302  zrhnm  30338  qqhnm  30359  measvunilem  30600  volfiniune  30618  dya2iocnrect  30668  sibfinima  30726  probun  30806  probinc  30808  cndprob01  30822  bnj517  31278  bnj594  31305  pconnpi1  31542  cvmsss2  31579  mrsubcv  31730  msubvrs  31780  dvdspw  31958  br6  31969  br4  31970  frpomin  32059  frrlem4  32104  nosep1o  32153  nosepssdm  32157  nolt02olem  32165  nosupres  32174  nosupbnd1lem1  32175  nosupbnd1lem4  32178  nosupbnd1lem5  32179  nosupbnd1lem6  32180  nosupbnd2  32183  noetalem2  32185  cgrcomim  32417  cgrtriv  32430  cgrextend  32436  segconeq  32438  btwntriv2  32440  btwnintr  32447  btwnexch3  32448  btwnouttr2  32450  trisegint  32456  cgrsub  32473  cgrxfr  32483  btwnxfr  32484  lineext  32504  btwnconn1lem13  32527  btwnconn1lem14  32528  btwnconn3  32531  segcon2  32533  brsegle  32536  brsegle2  32537  segletr  32542  segleantisym  32543  seglelin  32544  outsideofeu  32559  lineunray  32575  lineelsb2  32576  ivthALT  32651  lindsenlbs  33717  areacirc  33817  cocanfo  33824  upixp  33836  ismtyima  33913  rrndstprj2  33941  zerdivemp1x  34057  lsatfixedN  34789  lssat  34796  eqlkr  34879  eqlkr2  34880  lkrlsp  34882  lshpkrlem4  34893  opposet  34961  cvrcon3b  35057  cvrcmp  35063  atlen0  35090  atnle  35097  atlatmstc  35099  cvlatexch3  35118  cvlsupr2  35123  hlsupr2  35167  hlrelat2  35183  cvrexchlem  35199  lnnat  35207  atcvrj2b  35212  atle  35216  atexchcvrN  35220  atbtwn  35226  athgt  35236  3dimlem3  35241  3dim1  35247  1cvratlt  35254  1cvrjat  35255  ps-1  35257  ps-2  35258  3atlem3  35265  3atlem5  35267  3atlem7  35269  llni  35288  llni2  35292  atcvrlln2  35299  llnexatN  35301  llncmp  35302  2llnmat  35304  2at0mat0  35305  lplni  35312  lplnnle2at  35321  2atnelpln  35324  lplnllnneN  35336  llncvrlpln2  35337  2lplnmN  35339  2llnmj  35340  lplncmp  35342  lplnexatN  35343  lplnexllnN  35344  2llnm3N  35349  lvoli  35355  lvoli3  35357  islvol2aN  35372  4atlem0a  35373  4atlem3  35376  4atlem3a  35377  4atlem4a  35379  4atlem4b  35380  4atlem4c  35381  4atlem4d  35382  4atlem10b  35385  4atlem11  35389  4atlem12  35392  lplncvrlvol2  35395  lvolcmp  35397  2lplnmj  35402  islinei  35520  pmapglbx  35549  linepmap  35555  lneq2at  35558  lnjatN  35560  lncvrat  35562  lncmp  35563  2llnma3r  35568  elpaddatriN  35583  elpaddat  35584  paddcom  35593  paddss1  35597  paddss2  35598  paddss12  35599  paddasslem6  35605  paddasslem7  35606  paddasslem8  35607  paddasslem9  35608  paddasslem15  35614  pmodlem2  35627  pmodl42N  35631  pmapjoin  35632  llnmod1i2  35640  2polcon4bN  35698  polcon2bN  35700  poml4N  35733  poml6N  35735  osumcllem1N  35736  osumcllem2N  35737  osumcllem11N  35746  osumclN  35747  pmapojoinN  35748  pexmidlem2N  35751  pexmidlem3N  35752  pexmidlem4N  35753  pexmidlem6N  35755  pexmidlem7N  35756  pl42lem2N  35760  pl42lem3N  35761  pl42lem4N  35762  pl42N  35763  lhpexle2lem  35789  lhpexle3lem  35791  lhpexle3  35792  lhpmcvr3  35805  lhp2at0nle  35815  lhprelat3N  35820  4atex  35856  4atex2  35857  lauteq  35875  lautco  35877  ltrncoidN  35908  ltrneq2  35928  ltrnnidn  35955  ltrnideq  35956  trlnid  35960  ltrnatlw  35964  trlnle  35967  trlval3  35968  trlval4  35969  cdlemc  35978  cdlemd5  35983  cdlemd9  35987  ltrneq3  35989  cdleme0moN  36006  cdleme20  36105  cdleme21j  36117  cdleme21  36118  cdleme27cl  36147  cdlemefrs29bpre0  36177  cdlemefs27cl  36194  cdlemefs32sn1aw  36195  cdleme43fsv1snlem  36201  cdleme32d  36225  cdleme32f  36227  cdleme32le  36228  cdleme35h2  36238  cdleme38n  36245  cdleme40m  36248  cdleme41snaw  36257  cdleme42ke  36266  cdleme17d3  36277  cdleme48fvg  36281  cdlemeg46fvcl  36287  cdlemeg46fgN  36315  cdleme48gfv1  36317  cdleme48fgv  36319  cdleme50trn3  36334  trlord  36350  ltrniotavalbN  36365  cdlemb3  36387  cdlemg6c  36401  cdlemg6  36404  cdlemg7N  36407  cdlemg8c  36410  cdlemg8  36412  cdlemg11a  36418  cdlemg11b  36423  cdlemg12e  36428  cdlemg15a  36436  cdlemg15  36437  cdlemg16  36438  cdlemg16z  36440  cdlemg16zz  36441  cdlemg17dN  36444  cdlemg18a  36459  cdlemg20  36466  cdlemg22  36468  cdlemg24  36469  cdlemg37  36470  cdlemg31d  36481  cdlemg29  36486  cdlemg33b  36488  cdlemg33  36492  cdlemg38  36496  cdlemg39  36497  cdlemg40  36498  trlco  36508  trlcone  36509  cdlemg42  36510  cdlemg44b  36513  ltrncom  36519  trljco  36521  tendococl  36553  tendoplcl  36562  tendoplcom  36563  cdlemj2  36603  cdlemj3  36604  tendoid0  36606  tendoconid  36610  tendotr  36611  cdlemk25-3  36685  cdlemk26b-3  36686  cdlemk34  36691  cdlemk36  36694  cdlemk38  36696  cdlemkid4  36715  cdlemk35s-id  36719  cdlemk39s-id  36721  cdlemk19x  36724  cdlemk53  36738  cdlemk55  36742  cdlemk55u  36747  cdlemk39u  36749  cdlemk19u  36751  cdlemk56  36752  tendoex  36756  cdleml3N  36759  cdleml5N  36761  tendospcanN  36804  cdlemm10N  36899  cdlemn11pre  36991  dihord2pre  37006  dihvalcqpre  37016  dihopelvalcpre  37029  dihord6apre  37037  dihord5b  37040  dihord5apre  37043  dihord  37045  dihmeetlem1N  37071  dihglblem5apreN  37072  dihglblem3N  37076  dihmeetlem2N  37080  dihglbcpreN  37081  dihmeetbN  37084  dihmeetlem4preN  37087  dihmeetlem5  37089  dihmeetlem7N  37091  dihmeetlem10N  37097  dihmeetlem11N  37098  dihmeetlem12N  37099  dihmeetlem13N  37100  dihmeetlem15N  37102  dihmeetlem16N  37103  dihmeetlem17N  37104  dihmeetlem18N  37105  dihmeetlem19N  37106  dihmeetALTN  37108  dih1dimatlem0  37109  dihlspsnssN  37113  dihlspsnat  37114  mapdh8ad  37560  hdmap14lem14  37662  hgmapvvlem3  37706  mzprename  37814  eldioph2lem1  37825  lzunuz  37833  rencldnfi  37887  pellexlem2  37896  infmrgelbi  37944  pellfundglb  37951  pellfund14gap  37953  qirropth  37974  rmxycomplete  37983  congadd  38034  acongeq  38051  jm2.19  38061  jm2.23  38064  jm2.20nn  38065  jm2.27  38076  jm3.1  38088  aomclem6  38130  lnmepi  38156  lmhmfgsplit  38157  lmhmlnmsplit  38158  pwssplit4  38160  hbtlem2  38195  hbtlem5  38199  dgraa0p  38220  proot1hash  38279  iocunico  38296  relexpxpmin  38509  brtrclfv2  38519  ntrclsiso  38865  ntrclskb  38867  ntrclsk3  38868  k0004lem3  38947  suprnmpt  39844  wessf1ornlem  39860  projf1o  39875  snunioo1  40219  iccintsng  40230  lptre2pt  40352  limcleqr  40356  fnlimfvre  40386  limsupgtlem  40489  volioc  40667  iblspltprt  40668  stoweidlem19  40715  stoweidlem20  40716  stoweidlem22  40718  stoweidlem28  40724  stoweidlem34  40730  stoweidlem44  40740  stoweidlem60  40756  wallispilem3  40763  fourierdlem41  40844  fourierdlem42  40845  fourierdlem49  40851  fourierdlem51  40853  fourierdlem54  40856  fourierdlem74  40876  fourierdlem97  40899  caratheodorylem2  41223  ovnsubaddlem2  41267  hspmbllem2  41323  smflimmpt  41498  smflimsupmpt  41517  smfliminfmpt  41520  fzopredsuc  41908  fzoopth  41912  iccpartigtl  41934  repswpfx  42011  lighneal  42103  oexpnegALTV  42163  oexpnegnz  42164  tgblthelfgott  42278  lidldomn1  42489  ofaddmndmap  42690  lincdifsn  42781  lincellss  42783  lincresunit3lem3  42831  islindeps2  42840  lindssnlvec  42843  fdivmptf  42903  refdivmptf  42904
  Copyright terms: Public domain W3C validator