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

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

Proof of Theorem simp1l
StepHypRef Expression
1 simpl 483 . 2 ((𝜑𝜓) → 𝜑)
213ad2ant1 1125 1 (((𝜑𝜓) ∧ 𝜒𝜃) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1079
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 208  df-an 397  df-3an 1081
This theorem is referenced by:  simp11l  1276  simp21l  1282  simp31l  1288  tfisi  7561  offsplitfpar  7806  omeulem2  8199  uniinqs  8367  unxpdomlem3  8713  elfiun  8883  cantnffval  9115  tcrank  9302  cofsmo  9680  isfin2-2  9730  tskint  10196  tskun  10197  tskurn  10200  gruina  10229  dedekind  10792  subaddmulsub  11092  dmdcan  11339  lt2msq1  11513  supmullem1  11600  supmul  11602  xaddass  12632  xaddass2  12633  xlt2add  12643  xmulasslem3  12669  xadddi2r  12681  iccsplit  12861  expaddzlem  13462  expaddz  13463  expmulz  13465  ccatopth2  14069  pfxccat3  14086  resqrtcl  14603  limsupgle  14824  o1add  14960  o1mul  14961  o1sub  14962  bitsfzo  15774  sadfval  15791  smufval  15816  prmexpb  16052  4sqlem18  16288  vdwlem10  16316  fsets  16506  setsstruct2  16511  submre  16866  mrelatlub  17786  gsmsymgreqlem2  18490  mndodcong  18601  subgabl  18887  gex2abl  18902  cntzsubr  19499  abvres  19541  lbsind2  19784  lspsneu  19826  lbsextlem2  19862  lbsextg  19865  lindfind2  20892  matring  20982  maducoeval  21178  maducoeval2  21179  maduf  21180  madurid  21183  gsummatr01  21198  cramerimplem3  21224  cnprest  21827  hausnei2  21891  isreg2  21915  cmpcld  21940  llyrest  22023  nllyrest  22024  csdfil  22432  hausflimlem  22517  ssblps  22961  ssbl  22962  cphassi  23747  cphassir  23748  4cphipval2  23774  cphipval  23775  dvres2  24439  plyadd  24736  plymul  24737  coeeu  24744  vieta1  24830  aalioulem3  24852  aalioulem4  24853  efgh  25052  cxpadd  25189  cxpsub  25192  mulcxp  25195  divcxp  25197  cxple2  25207  cxplt2  25208  cxpcn3lem  25255  angcan  25307  ang180lem5  25318  isosctrlem3  25325  logexprlim  25729  lgssq  25841  abvcxp  26119  padicabv  26134  brbtwn2  26619  ax5seglem6  26648  axcontlem4  26681  axcontlem8  26685  uhgr2edg  26918  nbgrisvtx  27051  nbupgrres  27074  clwwlkccat  27696  clwwlknonex2lem2  27815  frgrreggt1  28100  chscllem4  29345  cshwrnid  30563  ogrpinvlt  30652  eqfunresadj  32902  poseq  32993  nosupbnd2lem1  33113  noetalem5  33119  ifscgr  33403  matunitlindflem1  34770  lshpnelb  36002  lfl1  36088  lshpkrlem6  36133  lshpkrex  36136  hlrelat3  36430  atbtwnexOLDN  36465  atbtwnex  36466  3dim3  36487  3atlem5  36505  2llnmat  36542  lvolex3N  36556  lvolnle3at  36600  4atlem11  36627  4atlem12  36630  dalemccea  36701  cdlema2N  36810  paddasslem2  36839  atmod1i1m  36876  lhp2lt  37019  lhp0lt  37021  lhpj1  37040  lhpmcvr4N  37044  lhpelim  37055  lhpmod2i2  37056  lhpmod6i1  37057  cdlemb2  37059  lhple  37060  lhpat  37061  4atex  37094  4atex2-0aOLDN  37096  4atex3  37099  ldilco  37134  ltrncl  37143  ltrn11  37144  ltrnle  37147  ltrncnvleN  37148  ltrnm  37149  ltrnj  37150  ltrncvr  37151  ltrnatb  37155  ltrnel  37157  ltrncnvel  37160  ltrncnv  37164  trlval2  37181  trlcnv  37183  trljat1  37184  trljat2  37185  trl0  37188  ltrnnidn  37192  trlnidatb  37195  cdlemc1  37209  cdlemc2  37210  cdlemc5  37213  cdlemc6  37214  cdlemd3  37218  cdlemd6  37221  cdleme0aa  37228  cdleme0b  37230  cdleme0c  37231  cdleme0e  37235  cdleme0fN  37236  cdleme01N  37239  cdleme02N  37240  cdleme0ex1N  37241  cdleme0moN  37243  cdleme3g  37252  cdleme3h  37253  cdleme3  37255  cdleme4  37256  cdleme4a  37257  cdleme5  37258  cdleme8  37268  cdleme9  37271  cdleme10  37272  cdleme16aN  37277  cdleme11a  37278  cdleme11fN  37282  cdleme11g  37283  cdleme11h  37284  cdleme11j  37285  cdleme11k  37286  cdleme12  37289  cdleme13  37290  cdleme17c  37306  cdleme17d1  37307  cdleme18a  37309  cdleme18b  37310  cdleme18c  37311  cdleme22gb  37312  cdlemeda  37316  cdlemednpq  37317  cdlemednuN  37318  cdleme19c  37323  cdleme20aN  37327  cdleme20bN  37328  cdleme20c  37329  cdleme22aa  37357  cdleme22a  37358  cdleme22b  37359  cdleme22d  37361  cdleme22e  37362  cdleme27cl  37384  cdleme27a  37385  cdleme30a  37396  cdleme42a  37489  cdleme42c  37490  cdleme50laut  37565  cdlemf1  37579  cdlemf  37581  cdlemfnid  37582  trlord  37587  cdlemg2fv2  37618  cdlemg2kq  37620  cdlemg2m  37622  cdlemg4a  37626  cdlemg4d  37631  cdlemg4g  37634  cdlemg4  37635  cdlemg6c  37638  cdlemg7aN  37643  cdlemg8a  37645  cdlemg8b  37646  cdlemg8c  37647  cdlemg9a  37650  cdlemg9b  37651  cdlemg9  37652  cdlemg11aq  37656  cdlemg10c  37657  cdlemg12a  37661  cdlemg12b  37662  cdlemg12c  37663  cdlemg17a  37679  cdlemg18b  37697  cdlemg18c  37698  cdlemg31b0a  37713  cdlemg31a  37715  cdlemg31b  37716  cdlemg31d  37718  cdlemg35  37731  trlcoabs2N  37740  trlcolem  37744  cdlemg44a  37749  trljco  37758  trljco2  37759  tendoco2  37786  tendopltp  37798  cdlemi1  37836  cdlemi2  37837  cdlemj3  37841  tendocan  37842  cdlemk3  37851  cdlemk4  37852  cdlemk5a  37853  cdlemk9  37857  cdlemk9bN  37858  cdlemkvcl  37860  cdlemk10  37861  cdlemk30  37912  cdlemk31  37914  cdlemk39  37934  cdlemkfid1N  37939  cdlemkid1  37940  cdlemkid2  37942  cdlemkfid3N  37943  cdlemk19ylem  37948  cdlemk19xlem  37960  cdlemk19x  37961  cdlemk53b  37974  cdlemk53  37975  cdlemk54  37976  cdlemk55a  37977  cdlemk43N  37981  cdlemk19u1  37987  cdlemk19u  37988  cdleml1N  37994  erngdvlem4  38009  erngdvlem4-rN  38017  dia11N  38066  cdlemm10N  38136  dib11N  38178  cdlemn2  38213  cdlemn10  38224  dihjustlem  38234  dihord2cN  38239  dihlsscpre  38252  dih1dimb2  38259  dihvalcq2  38265  dihopelvalcpre  38266  dihord6b  38278  dih11  38283  dihmeetlem1N  38308  dihglblem2N  38312  dihglblem3N  38313  dihmeetlem2N  38317  dihglbcpreN  38318  dihmeetcN  38320  dihmeetbclemN  38322  dihmeetlem4preN  38324  dihmeetlem9N  38333  dihmeetlem20N  38344  dihlspsnssN  38350  dihlspsnat  38351  dihatlat  38352  dihglblem6  38358  dihmeet  38361  dochss  38383  hdmapval3N  38856  hgmap11  38920  nn0rppwr  39062  remulcand  39130  congtr  39442  fzmaxdif  39458  isnumbasgrplem2  39584  ntrclsk13  40301  ssmapsn  41359  infleinf  41520  suplesup2  41524  supxrunb3  41552  mullimc  41777  mullimcf  41784  islpcn  41800  limsupresxr  41927  liminfresxr  41928  cncfuni  42049  icccncfext  42050  stoweidlem34  42200  stoweidlem59  42225  stirlinglem13  42252  fourierdlem41  42314  fourierdlem42  42315  fourierdlem73  42345  sge0iunmptlemfi  42576  meadjiunlem  42628  ovncvrrp  42727  sssmf  42896  smflimsuplem7  42981  smflimsuplem8  42982  funressneu  43163  lincscm  44383  lincext3  44409  el0ldep  44419  el0ldepsnzr  44420  itscnhlc0xyqsol  44650
  Copyright terms: Public domain W3C validator