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

Theorem simp1l 1083
Description: Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
Assertion
Ref Expression
simp1l (((𝜑𝜓) ∧ 𝜒𝜃) → 𝜑)

Proof of Theorem simp1l
StepHypRef Expression
1 simpl 473 . 2 ((𝜑𝜓) → 𝜑)
213ad2ant1 1080 1 (((𝜑𝜓) ∧ 𝜒𝜃) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1036
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 197  df-an 386  df-3an 1038
This theorem is referenced by:  simpl1l  1110  simpr1l  1116  simp11l  1170  simp21l  1176  simp31l  1182  funprgOLD  5909  tfisi  7020  omeulem2  7623  uniinqs  7787  unxpdomlem3  8126  elfiun  8296  cantnffval  8520  tcrank  8707  cofsmo  9051  isfin2-2  9101  tskint  9567  tskun  9568  tskurn  9571  gruina  9600  dedekind  10160  dmdcan  10695  lt2msq1  10867  supmullem1  10953  supmul  10955  xaddass  12038  xaddass2  12039  xlt2add  12049  xmulasslem3  12075  xadddi2r  12087  iccsplit  12263  expaddzlem  12859  expaddz  12860  expmulz  12862  ccatopth2  13425  swrdccat3  13445  resqrtcl  13944  limsupgle  14158  o1add  14294  o1mul  14295  o1sub  14296  bitsfzo  15100  sadfval  15117  smufval  15142  prmexpb  15373  4sqlem18  15609  vdwlem10  15637  fsets  15831  setsstruct2  15836  submre  16205  mrelatlub  17126  mndodcong  17901  subgabl  18181  gex2abl  18194  cntzsubr  18752  abvres  18779  lbsind2  19021  lspsneu  19063  lbsextlem2  19099  lbsextg  19102  lindfind2  20097  matring  20189  maducoeval  20385  maducoeval2  20386  maduf  20387  madurid  20390  gsummatr01  20405  cramerimplem3  20431  cnprest  21033  hausnei2  21097  isreg2  21121  cmpcld  21145  llyrest  21228  nllyrest  21229  csdfil  21638  hausflimlem  21723  ssblps  22167  ssbl  22168  cphassi  22954  cphassir  22955  4cphipval2  22981  cphipval  22982  dvres2  23616  plyadd  23911  plymul  23912  coeeu  23919  vieta1  24005  aalioulem3  24027  aalioulem4  24028  efgh  24225  cxpadd  24359  cxpsub  24362  mulcxp  24365  divcxp  24367  cxple2  24377  cxplt2  24378  cxpcn3lem  24422  angcan  24466  ang180lem5  24477  isosctrlem3  24484  logexprlim  24884  lgssq  24996  abvcxp  25238  padicabv  25253  brbtwn2  25719  ax5seglem6  25748  axcontlem4  25781  axcontlem8  25785  uhgr2edg  26027  nbgrisvtx  26176  nbupgrres  26187  frgrreggt1  27139  chscllem4  28387  ogrpinvlt  29551  poseq  31504  wsuclemOLD  31528  ifscgr  31846  matunitlindflem1  33076  lshpnelb  33790  lfl1  33876  lshpkrlem6  33921  lshpkrex  33924  hlrelat3  34217  atbtwnexOLDN  34252  atbtwnex  34253  3dim3  34274  3atlem5  34292  2llnmat  34329  lvolex3N  34343  lvolnle3at  34387  4atlem11  34414  4atlem12  34417  dalemccea  34488  cdlema2N  34597  paddasslem2  34626  atmod1i1m  34663  lhp2lt  34806  lhp0lt  34808  lhpj1  34827  lhpmcvr4N  34831  lhpelim  34842  lhpmod2i2  34843  lhpmod6i1  34844  cdlemb2  34846  lhple  34847  lhpat  34848  4atex  34881  4atex2-0aOLDN  34883  4atex3  34886  ldilco  34921  ltrncl  34930  ltrn11  34931  ltrnle  34934  ltrncnvleN  34935  ltrnm  34936  ltrnj  34937  ltrncvr  34938  ltrnatb  34942  ltrnel  34944  ltrncnvel  34947  ltrncnv  34951  ltrnmwOLD  34957  trlval2  34969  trlcnv  34971  trljat1  34972  trljat2  34973  trl0  34976  ltrnnidn  34980  trlnidatb  34983  cdlemc1  34997  cdlemc2  34998  cdlemc5  35001  cdlemc6  35002  cdlemd3  35006  cdlemd6  35009  cdleme0aa  35016  cdleme0b  35018  cdleme0c  35019  cdleme0e  35023  cdleme0fN  35024  cdleme01N  35027  cdleme02N  35028  cdleme0ex1N  35029  cdleme0moN  35031  cdleme3g  35040  cdleme3h  35041  cdleme3  35043  cdleme4  35044  cdleme4a  35045  cdleme5  35046  cdleme8  35056  cdleme9  35059  cdleme10  35060  cdleme16aN  35065  cdleme11a  35066  cdleme11fN  35070  cdleme11g  35071  cdleme11h  35072  cdleme11j  35073  cdleme11k  35074  cdleme12  35077  cdleme13  35078  cdleme17c  35094  cdleme17d1  35095  cdleme18a  35097  cdleme18b  35098  cdleme18c  35099  cdleme22gb  35100  cdlemeda  35104  cdlemednpq  35105  cdlemednuN  35106  cdleme19c  35112  cdleme20aN  35116  cdleme20bN  35117  cdleme20c  35118  cdleme22aa  35146  cdleme22a  35147  cdleme22b  35148  cdleme22d  35150  cdleme22e  35151  cdleme27cl  35173  cdleme27a  35174  cdleme30a  35185  cdleme42a  35278  cdleme42c  35279  cdleme50laut  35354  cdlemf1  35368  cdlemf  35370  cdlemfnid  35371  trlord  35376  cdlemg2fv2  35407  cdlemg2kq  35409  cdlemg2m  35411  cdlemg4a  35415  cdlemg4d  35420  cdlemg4g  35423  cdlemg4  35424  cdlemg6c  35427  cdlemg7aN  35432  cdlemg8a  35434  cdlemg8b  35435  cdlemg8c  35436  cdlemg9a  35439  cdlemg9b  35440  cdlemg9  35441  cdlemg11aq  35445  cdlemg10c  35446  cdlemg12a  35450  cdlemg12b  35451  cdlemg12c  35452  cdlemg17a  35468  cdlemg18b  35486  cdlemg18c  35487  cdlemg31b0a  35502  cdlemg31a  35504  cdlemg31b  35505  cdlemg31d  35507  cdlemg35  35520  trlcoabs2N  35529  trlcolem  35533  cdlemg44a  35538  trljco  35547  trljco2  35548  tendoco2  35575  tendopltp  35587  cdlemi1  35625  cdlemi2  35626  cdlemj3  35630  tendocan  35631  cdlemk3  35640  cdlemk4  35641  cdlemk5a  35642  cdlemk9  35646  cdlemk9bN  35647  cdlemkvcl  35649  cdlemk10  35650  cdlemk30  35701  cdlemk31  35703  cdlemk39  35723  cdlemkfid1N  35728  cdlemkid1  35729  cdlemkid2  35731  cdlemkfid3N  35732  cdlemk19ylem  35737  cdlemk19xlem  35749  cdlemk19x  35750  cdlemk53b  35763  cdlemk53  35764  cdlemk54  35765  cdlemk55a  35766  cdlemk43N  35770  cdlemk19u1  35776  cdlemk19u  35777  cdleml1N  35783  erngdvlem4  35798  erngdvlem4-rN  35806  dia11N  35856  cdlemm10N  35926  dib11N  35968  cdlemn2  36003  cdlemn10  36014  dihjustlem  36024  dihord2cN  36029  dihlsscpre  36042  dih1dimb2  36049  dihvalcq2  36055  dihopelvalcpre  36056  dihord6b  36068  dih11  36073  dihmeetlem1N  36098  dihglblem2N  36102  dihglblem3N  36103  dihmeetlem2N  36107  dihglbcpreN  36108  dihmeetcN  36110  dihmeetbclemN  36112  dihmeetlem4preN  36114  dihmeetlem9N  36123  dihmeetlem20N  36134  dihlspsnssN  36140  dihlspsnat  36141  dihatlat  36142  dihglblem6  36148  dihmeet  36151  dochss  36173  hdmapval3N  36649  hgmap11  36713  congtr  37051  fzmaxdif  37067  isnumbasgrplem2  37194  ntrclsk13  37890  ssmapsn  38917  infleinf  39087  suplesup2  39091  supxrunb3  39122  mullimc  39284  mullimcf  39291  islpcn  39307  cncfuni  39434  icccncfext  39435  stoweidlem34  39588  stoweidlem59  39613  stirlinglem13  39640  fourierdlem41  39702  fourierdlem42  39703  fourierdlem73  39733  sge0iunmptlemfi  39967  meadjiunlem  40019  ovncvrrp  40115  sssmf  40284  smflimsuplem7  40369  smflimsuplem8  40370  pfxccat3  40755  lincscm  41537  lincext3  41563  el0ldep  41573  el0ldepsnzr  41574
  Copyright terms: Public domain W3C validator