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

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

Proof of Theorem simp1l
StepHypRef Expression
1 simpl 472 . 2 ((𝜑𝜓) → 𝜑)
213ad2ant1 1102 1 (((𝜑𝜓) ∧ 𝜒𝜃) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1054
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 385  df-3an 1056
This theorem is referenced by:  simpl1l  1132  simpr1l  1138  simp11l  1192  simp21l  1198  simp31l  1204  funprgOLD  5979  tfisi  7100  omeulem2  7708  uniinqs  7870  unxpdomlem3  8207  elfiun  8377  cantnffval  8598  tcrank  8785  cofsmo  9129  isfin2-2  9179  tskint  9645  tskun  9646  tskurn  9649  gruina  9678  dedekind  10238  dmdcan  10773  lt2msq1  10945  supmullem1  11031  supmul  11033  xaddass  12117  xaddass2  12118  xlt2add  12128  xmulasslem3  12154  xadddi2r  12166  iccsplit  12343  expaddzlem  12943  expaddz  12944  expmulz  12946  ccatopth2  13517  swrdccat3  13538  resqrtcl  14038  limsupgle  14252  o1add  14388  o1mul  14389  o1sub  14390  bitsfzo  15204  sadfval  15221  smufval  15246  prmexpb  15477  4sqlem18  15713  vdwlem10  15741  fsets  15938  setsstruct2  15943  submre  16312  mrelatlub  17233  mndodcong  18007  subgabl  18287  gex2abl  18300  cntzsubr  18860  abvres  18887  lbsind2  19129  lspsneu  19171  lbsextlem2  19207  lbsextg  19210  lindfind2  20205  matring  20297  maducoeval  20493  maducoeval2  20494  maduf  20495  madurid  20498  gsummatr01  20513  cramerimplem3  20539  cnprest  21141  hausnei2  21205  isreg2  21229  cmpcld  21253  llyrest  21336  nllyrest  21337  csdfil  21745  hausflimlem  21830  ssblps  22274  ssbl  22275  cphassi  23060  cphassir  23061  4cphipval2  23087  cphipval  23088  dvres2  23721  plyadd  24018  plymul  24019  coeeu  24026  vieta1  24112  aalioulem3  24134  aalioulem4  24135  efgh  24332  cxpadd  24470  cxpsub  24473  mulcxp  24476  divcxp  24478  cxple2  24488  cxplt2  24489  cxpcn3lem  24533  angcan  24577  ang180lem5  24588  isosctrlem3  24595  logexprlim  24995  lgssq  25107  abvcxp  25349  padicabv  25364  brbtwn2  25830  ax5seglem6  25859  axcontlem4  25892  axcontlem8  25896  uhgr2edg  26145  nbgrisvtx  26280  nbgrisvtxOLD  26282  nbupgrres  26310  clwwlkccat  27332  frgrreggt1  27380  chscllem4  28627  ogrpinvlt  29852  eqfunresadj  31785  poseq  31878  nosupbnd2lem1  31986  noetalem5  31992  ifscgr  32276  matunitlindflem1  33535  lshpnelb  34589  lfl1  34675  lshpkrlem6  34720  lshpkrex  34723  hlrelat3  35016  atbtwnexOLDN  35051  atbtwnex  35052  3dim3  35073  3atlem5  35091  2llnmat  35128  lvolex3N  35142  lvolnle3at  35186  4atlem11  35213  4atlem12  35216  dalemccea  35287  cdlema2N  35396  paddasslem2  35425  atmod1i1m  35462  lhp2lt  35605  lhp0lt  35607  lhpj1  35626  lhpmcvr4N  35630  lhpelim  35641  lhpmod2i2  35642  lhpmod6i1  35643  cdlemb2  35645  lhple  35646  lhpat  35647  4atex  35680  4atex2-0aOLDN  35682  4atex3  35685  ldilco  35720  ltrncl  35729  ltrn11  35730  ltrnle  35733  ltrncnvleN  35734  ltrnm  35735  ltrnj  35736  ltrncvr  35737  ltrnatb  35741  ltrnel  35743  ltrncnvel  35746  ltrncnv  35750  ltrnmwOLD  35756  trlval2  35768  trlcnv  35770  trljat1  35771  trljat2  35772  trl0  35775  ltrnnidn  35779  trlnidatb  35782  cdlemc1  35796  cdlemc2  35797  cdlemc5  35800  cdlemc6  35801  cdlemd3  35805  cdlemd6  35808  cdleme0aa  35815  cdleme0b  35817  cdleme0c  35818  cdleme0e  35822  cdleme0fN  35823  cdleme01N  35826  cdleme02N  35827  cdleme0ex1N  35828  cdleme0moN  35830  cdleme3g  35839  cdleme3h  35840  cdleme3  35842  cdleme4  35843  cdleme4a  35844  cdleme5  35845  cdleme8  35855  cdleme9  35858  cdleme10  35859  cdleme16aN  35864  cdleme11a  35865  cdleme11fN  35869  cdleme11g  35870  cdleme11h  35871  cdleme11j  35872  cdleme11k  35873  cdleme12  35876  cdleme13  35877  cdleme17c  35893  cdleme17d1  35894  cdleme18a  35896  cdleme18b  35897  cdleme18c  35898  cdleme22gb  35899  cdlemeda  35903  cdlemednpq  35904  cdlemednuN  35905  cdleme19c  35910  cdleme20aN  35914  cdleme20bN  35915  cdleme20c  35916  cdleme22aa  35944  cdleme22a  35945  cdleme22b  35946  cdleme22d  35948  cdleme22e  35949  cdleme27cl  35971  cdleme27a  35972  cdleme30a  35983  cdleme42a  36076  cdleme42c  36077  cdleme50laut  36152  cdlemf1  36166  cdlemf  36168  cdlemfnid  36169  trlord  36174  cdlemg2fv2  36205  cdlemg2kq  36207  cdlemg2m  36209  cdlemg4a  36213  cdlemg4d  36218  cdlemg4g  36221  cdlemg4  36222  cdlemg6c  36225  cdlemg7aN  36230  cdlemg8a  36232  cdlemg8b  36233  cdlemg8c  36234  cdlemg9a  36237  cdlemg9b  36238  cdlemg9  36239  cdlemg11aq  36243  cdlemg10c  36244  cdlemg12a  36248  cdlemg12b  36249  cdlemg12c  36250  cdlemg17a  36266  cdlemg18b  36284  cdlemg18c  36285  cdlemg31b0a  36300  cdlemg31a  36302  cdlemg31b  36303  cdlemg31d  36305  cdlemg35  36318  trlcoabs2N  36327  trlcolem  36331  cdlemg44a  36336  trljco  36345  trljco2  36346  tendoco2  36373  tendopltp  36385  cdlemi1  36423  cdlemi2  36424  cdlemj3  36428  tendocan  36429  cdlemk3  36438  cdlemk4  36439  cdlemk5a  36440  cdlemk9  36444  cdlemk9bN  36445  cdlemkvcl  36447  cdlemk10  36448  cdlemk30  36499  cdlemk31  36501  cdlemk39  36521  cdlemkfid1N  36526  cdlemkid1  36527  cdlemkid2  36529  cdlemkfid3N  36530  cdlemk19ylem  36535  cdlemk19xlem  36547  cdlemk19x  36548  cdlemk53b  36561  cdlemk53  36562  cdlemk54  36563  cdlemk55a  36564  cdlemk43N  36568  cdlemk19u1  36574  cdlemk19u  36575  cdleml1N  36581  erngdvlem4  36596  erngdvlem4-rN  36604  dia11N  36654  cdlemm10N  36724  dib11N  36766  cdlemn2  36801  cdlemn10  36812  dihjustlem  36822  dihord2cN  36827  dihlsscpre  36840  dih1dimb2  36847  dihvalcq2  36853  dihopelvalcpre  36854  dihord6b  36866  dih11  36871  dihmeetlem1N  36896  dihglblem2N  36900  dihglblem3N  36901  dihmeetlem2N  36905  dihglbcpreN  36906  dihmeetcN  36908  dihmeetbclemN  36910  dihmeetlem4preN  36912  dihmeetlem9N  36921  dihmeetlem20N  36932  dihlspsnssN  36938  dihlspsnat  36939  dihatlat  36940  dihglblem6  36946  dihmeet  36949  dochss  36971  hdmapval3N  37447  hgmap11  37511  congtr  37849  fzmaxdif  37865  isnumbasgrplem2  37991  ntrclsk13  38686  ssmapsn  39722  infleinf  39901  suplesup2  39905  supxrunb3  39936  mullimc  40166  mullimcf  40173  islpcn  40189  limsupresxr  40316  liminfresxr  40317  cncfuni  40417  icccncfext  40418  stoweidlem34  40569  stoweidlem59  40594  stirlinglem13  40621  fourierdlem41  40683  fourierdlem42  40684  fourierdlem73  40714  sge0iunmptlemfi  40948  meadjiunlem  41000  ovncvrrp  41099  sssmf  41268  smflimsuplem7  41353  smflimsuplem8  41354  pfxccat3  41751  lincscm  42544  lincext3  42570  el0ldep  42580  el0ldepsnzr  42581
  Copyright terms: Public domain W3C validator