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

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

Proof of Theorem simp1l
StepHypRef Expression
1 simpl 471 . 2 ((𝜑𝜓) → 𝜑)
213ad2ant1 1074 1 (((𝜑𝜓) ∧ 𝜒𝜃) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1030
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 195  df-an 384  df-3an 1032
This theorem is referenced by:  simpl1l  1104  simpr1l  1110  simp11l  1164  simp21l  1170  simp31l  1176  funprgOLD  5838  tfisi  6924  omeulem2  7524  uniinqs  7688  unxpdomlem3  8025  elfiun  8193  cantnffval  8417  tcrank  8604  cofsmo  8948  isfin2-2  8998  tskint  9460  tskun  9461  tskurn  9464  gruina  9493  dedekind  10048  dmdcan  10581  lt2msq1  10753  supmullem1  10837  supmul  10839  xaddass  11905  xaddass2  11906  xlt2add  11916  xmulasslem3  11942  xadddi2r  11954  iccsplit  12129  expaddzlem  12717  expaddz  12718  expmulz  12720  ccatopth2  13266  swrdccat3  13286  resqrtcl  13785  limsupgle  13999  o1add  14135  o1mul  14136  o1sub  14137  bitsfzo  14938  sadfval  14955  smufval  14980  prmexpb  15211  4sqlem18  15447  vdwlem10  15475  fsets  15666  submre  16031  mrelatlub  16952  mndodcong  17727  subgabl  18007  gex2abl  18020  cntzsubr  18578  abvres  18605  lbsind2  18845  lspsneu  18887  lbsextlem2  18923  lbsextg  18926  lindfind2  19915  matring  20007  maducoeval  20203  maducoeval2  20204  maduf  20205  madurid  20208  gsummatr01  20223  cramerimplem3  20249  cnprest  20842  hausnei2  20906  isreg2  20930  cmpcld  20954  llyrest  21037  nllyrest  21038  csdfil  21447  hausflimlem  21532  ssblps  21975  ssbl  21976  dvres2  23396  plyadd  23691  plymul  23692  coeeu  23699  vieta1  23785  aalioulem3  23807  aalioulem4  23808  efgh  24005  cxpadd  24139  cxpsub  24142  mulcxp  24145  divcxp  24147  cxple2  24157  cxplt2  24158  cxpcn3lem  24202  angcan  24246  ang180lem5  24257  isosctrlem3  24264  logexprlim  24664  lgssq  24776  abvcxp  25018  padicabv  25033  brbtwn2  25500  ax5seglem6  25529  axcontlem4  25562  axcontlem8  25566  clwwlknimp  26067  chscllem4  27686  ogrpinvlt  28858  poseq  30797  wsuclemOLD  30821  nofulllem5  30908  ifscgr  31124  matunitlindflem1  32375  lshpnelb  33089  lfl1  33175  lshpkrlem6  33220  lshpkrex  33223  hlrelat3  33516  atbtwnexOLDN  33551  atbtwnex  33552  3dim3  33573  3atlem5  33591  2llnmat  33628  lvolex3N  33642  lvolnle3at  33686  4atlem11  33713  4atlem12  33716  dalemccea  33787  cdlema2N  33896  paddasslem2  33925  atmod1i1m  33962  lhp2lt  34105  lhp0lt  34107  lhpj1  34126  lhpmcvr4N  34130  lhpelim  34141  lhpmod2i2  34142  lhpmod6i1  34143  cdlemb2  34145  lhple  34146  lhpat  34147  4atex  34180  4atex2-0aOLDN  34182  4atex3  34185  ldilco  34220  ltrncl  34229  ltrn11  34230  ltrnle  34233  ltrncnvleN  34234  ltrnm  34235  ltrnj  34236  ltrncvr  34237  ltrnatb  34241  ltrnel  34243  ltrncnvel  34246  ltrncnv  34250  ltrnmwOLD  34256  trlval2  34268  trlcnv  34270  trljat1  34271  trljat2  34272  trl0  34275  ltrnnidn  34279  trlnidatb  34282  cdlemc1  34296  cdlemc2  34297  cdlemc5  34300  cdlemc6  34301  cdlemd3  34305  cdlemd6  34308  cdleme0aa  34315  cdleme0b  34317  cdleme0c  34318  cdleme0e  34322  cdleme0fN  34323  cdleme01N  34326  cdleme02N  34327  cdleme0ex1N  34328  cdleme0moN  34330  cdleme3g  34339  cdleme3h  34340  cdleme3  34342  cdleme4  34343  cdleme4a  34344  cdleme5  34345  cdleme8  34355  cdleme9  34358  cdleme10  34359  cdleme16aN  34364  cdleme11a  34365  cdleme11fN  34369  cdleme11g  34370  cdleme11h  34371  cdleme11j  34372  cdleme11k  34373  cdleme12  34376  cdleme13  34377  cdleme17c  34393  cdleme17d1  34394  cdleme18a  34396  cdleme18b  34397  cdleme18c  34398  cdleme22gb  34399  cdlemeda  34403  cdlemednpq  34404  cdlemednuN  34405  cdleme19c  34411  cdleme20aN  34415  cdleme20bN  34416  cdleme20c  34417  cdleme22aa  34445  cdleme22a  34446  cdleme22b  34447  cdleme22d  34449  cdleme22e  34450  cdleme27cl  34472  cdleme27a  34473  cdleme30a  34484  cdleme42a  34577  cdleme42c  34578  cdleme50laut  34653  cdlemf1  34667  cdlemf  34669  cdlemfnid  34670  trlord  34675  cdlemg2fv2  34706  cdlemg2kq  34708  cdlemg2m  34710  cdlemg4a  34714  cdlemg4d  34719  cdlemg4g  34722  cdlemg4  34723  cdlemg6c  34726  cdlemg7aN  34731  cdlemg8a  34733  cdlemg8b  34734  cdlemg8c  34735  cdlemg9a  34738  cdlemg9b  34739  cdlemg9  34740  cdlemg11aq  34744  cdlemg10c  34745  cdlemg12a  34749  cdlemg12b  34750  cdlemg12c  34751  cdlemg17a  34767  cdlemg18b  34785  cdlemg18c  34786  cdlemg31b0a  34801  cdlemg31a  34803  cdlemg31b  34804  cdlemg31d  34806  cdlemg35  34819  trlcoabs2N  34828  trlcolem  34832  cdlemg44a  34837  trljco  34846  trljco2  34847  tendoco2  34874  tendopltp  34886  cdlemi1  34924  cdlemi2  34925  cdlemj3  34929  tendocan  34930  cdlemk3  34939  cdlemk4  34940  cdlemk5a  34941  cdlemk9  34945  cdlemk9bN  34946  cdlemkvcl  34948  cdlemk10  34949  cdlemk30  35000  cdlemk31  35002  cdlemk39  35022  cdlemkfid1N  35027  cdlemkid1  35028  cdlemkid2  35030  cdlemkfid3N  35031  cdlemk19ylem  35036  cdlemk19xlem  35048  cdlemk19x  35049  cdlemk53b  35062  cdlemk53  35063  cdlemk54  35064  cdlemk55a  35065  cdlemk43N  35069  cdlemk19u1  35075  cdlemk19u  35076  cdleml1N  35082  erngdvlem4  35097  erngdvlem4-rN  35105  dia11N  35155  cdlemm10N  35225  dib11N  35267  cdlemn2  35302  cdlemn10  35313  dihjustlem  35323  dihord2cN  35328  dihlsscpre  35341  dih1dimb2  35348  dihvalcq2  35354  dihopelvalcpre  35355  dihord6b  35367  dih11  35372  dihmeetlem1N  35397  dihglblem2N  35401  dihglblem3N  35402  dihmeetlem2N  35406  dihglbcpreN  35407  dihmeetcN  35409  dihmeetbclemN  35411  dihmeetlem4preN  35413  dihmeetlem9N  35422  dihmeetlem20N  35433  dihlspsnssN  35439  dihlspsnat  35440  dihatlat  35441  dihglblem6  35447  dihmeet  35450  dochss  35472  hdmapval3N  35948  hgmap11  36012  congtr  36350  fzmaxdif  36366  isnumbasgrplem2  36493  ntrclsk13  37189  ssmapsn  38203  infleinf  38330  suplesup2  38334  mullimc  38484  mullimcf  38491  islpcn  38507  cncfuni  38573  icccncfext  38574  stoweidlem34  38728  stoweidlem59  38753  stirlinglem13  38780  fourierdlem41  38842  fourierdlem42  38843  fourierdlem73  38873  sge0iunmptlemfi  39107  meadjiunlem  39159  ovncvrrp  39255  sssmf  39426  pfxccat3  40091  uhgr2edg  40434  nbgrisvtx  40580  nbupgrres  40591  av-frgrareggt1  41546  lincscm  42012  lincext3  42038  el0ldep  42048  el0ldepsnzr  42049
  Copyright terms: Public domain W3C validator