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

Theorem simp1l 1191
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 1127 1 (((𝜑𝜓) ∧ 𝜒𝜃) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1081
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 1083
This theorem is referenced by:  simp11l  1278  simp21l  1284  simp31l  1290  tfisi  7564  offsplitfpar  7809  omeulem2  8202  uniinqs  8370  unxpdomlem3  8716  elfiun  8886  cantnffval  9118  tcrank  9305  cofsmo  9683  isfin2-2  9733  tskint  10199  tskun  10200  tskurn  10203  gruina  10232  dedekind  10795  subaddmulsub  11095  dmdcan  11342  lt2msq1  11516  supmullem1  11603  supmul  11605  xaddass  12635  xaddass2  12636  xlt2add  12646  xmulasslem3  12672  xadddi2r  12684  iccsplit  12864  expaddzlem  13465  expaddz  13466  expmulz  13468  ccatopth2  14072  pfxccat3  14089  resqrtcl  14606  limsupgle  14827  o1add  14963  o1mul  14964  o1sub  14965  bitsfzo  15776  sadfval  15793  smufval  15818  prmexpb  16054  4sqlem18  16290  vdwlem10  16318  fsets  16508  setsstruct2  16513  submre  16868  mrelatlub  17788  gsmsymgreqlem2  18481  mndodcong  18592  subgabl  18878  gex2abl  18893  cntzsubr  19490  abvres  19532  lbsind2  19775  lspsneu  19817  lbsextlem2  19853  lbsextg  19856  lindfind2  20880  matring  20970  maducoeval  21166  maducoeval2  21167  maduf  21168  madurid  21171  gsummatr01  21186  cramerimplem3  21212  cnprest  21815  hausnei2  21879  isreg2  21903  cmpcld  21928  llyrest  22011  nllyrest  22012  csdfil  22420  hausflimlem  22505  ssblps  22949  ssbl  22950  cphassi  23735  cphassir  23736  4cphipval2  23762  cphipval  23763  dvres2  24427  plyadd  24724  plymul  24725  coeeu  24732  vieta1  24818  aalioulem3  24840  aalioulem4  24841  efgh  25040  cxpadd  25177  cxpsub  25180  mulcxp  25183  divcxp  25185  cxple2  25195  cxplt2  25196  cxpcn3lem  25243  angcan  25295  ang180lem5  25306  isosctrlem3  25313  logexprlim  25717  lgssq  25829  abvcxp  26107  padicabv  26122  brbtwn2  26607  ax5seglem6  26636  axcontlem4  26669  axcontlem8  26673  uhgr2edg  26906  nbgrisvtx  27039  nbupgrres  27062  clwwlkccat  27684  clwwlknonex2lem2  27803  frgrreggt1  28088  chscllem4  29333  cshwrnid  30551  ogrpinvlt  30640  eqfunresadj  32890  poseq  32981  nosupbnd2lem1  33101  noetalem5  33107  ifscgr  33391  matunitlindflem1  34757  lshpnelb  35989  lfl1  36075  lshpkrlem6  36120  lshpkrex  36123  hlrelat3  36417  atbtwnexOLDN  36452  atbtwnex  36453  3dim3  36474  3atlem5  36492  2llnmat  36529  lvolex3N  36543  lvolnle3at  36587  4atlem11  36614  4atlem12  36617  dalemccea  36688  cdlema2N  36797  paddasslem2  36826  atmod1i1m  36863  lhp2lt  37006  lhp0lt  37008  lhpj1  37027  lhpmcvr4N  37031  lhpelim  37042  lhpmod2i2  37043  lhpmod6i1  37044  cdlemb2  37046  lhple  37047  lhpat  37048  4atex  37081  4atex2-0aOLDN  37083  4atex3  37086  ldilco  37121  ltrncl  37130  ltrn11  37131  ltrnle  37134  ltrncnvleN  37135  ltrnm  37136  ltrnj  37137  ltrncvr  37138  ltrnatb  37142  ltrnel  37144  ltrncnvel  37147  ltrncnv  37151  trlval2  37168  trlcnv  37170  trljat1  37171  trljat2  37172  trl0  37175  ltrnnidn  37179  trlnidatb  37182  cdlemc1  37196  cdlemc2  37197  cdlemc5  37200  cdlemc6  37201  cdlemd3  37205  cdlemd6  37208  cdleme0aa  37215  cdleme0b  37217  cdleme0c  37218  cdleme0e  37222  cdleme0fN  37223  cdleme01N  37226  cdleme02N  37227  cdleme0ex1N  37228  cdleme0moN  37230  cdleme3g  37239  cdleme3h  37240  cdleme3  37242  cdleme4  37243  cdleme4a  37244  cdleme5  37245  cdleme8  37255  cdleme9  37258  cdleme10  37259  cdleme16aN  37264  cdleme11a  37265  cdleme11fN  37269  cdleme11g  37270  cdleme11h  37271  cdleme11j  37272  cdleme11k  37273  cdleme12  37276  cdleme13  37277  cdleme17c  37293  cdleme17d1  37294  cdleme18a  37296  cdleme18b  37297  cdleme18c  37298  cdleme22gb  37299  cdlemeda  37303  cdlemednpq  37304  cdlemednuN  37305  cdleme19c  37310  cdleme20aN  37314  cdleme20bN  37315  cdleme20c  37316  cdleme22aa  37344  cdleme22a  37345  cdleme22b  37346  cdleme22d  37348  cdleme22e  37349  cdleme27cl  37371  cdleme27a  37372  cdleme30a  37383  cdleme42a  37476  cdleme42c  37477  cdleme50laut  37552  cdlemf1  37566  cdlemf  37568  cdlemfnid  37569  trlord  37574  cdlemg2fv2  37605  cdlemg2kq  37607  cdlemg2m  37609  cdlemg4a  37613  cdlemg4d  37618  cdlemg4g  37621  cdlemg4  37622  cdlemg6c  37625  cdlemg7aN  37630  cdlemg8a  37632  cdlemg8b  37633  cdlemg8c  37634  cdlemg9a  37637  cdlemg9b  37638  cdlemg9  37639  cdlemg11aq  37643  cdlemg10c  37644  cdlemg12a  37648  cdlemg12b  37649  cdlemg12c  37650  cdlemg17a  37666  cdlemg18b  37684  cdlemg18c  37685  cdlemg31b0a  37700  cdlemg31a  37702  cdlemg31b  37703  cdlemg31d  37705  cdlemg35  37718  trlcoabs2N  37727  trlcolem  37731  cdlemg44a  37736  trljco  37745  trljco2  37746  tendoco2  37773  tendopltp  37785  cdlemi1  37823  cdlemi2  37824  cdlemj3  37828  tendocan  37829  cdlemk3  37838  cdlemk4  37839  cdlemk5a  37840  cdlemk9  37844  cdlemk9bN  37845  cdlemkvcl  37847  cdlemk10  37848  cdlemk30  37899  cdlemk31  37901  cdlemk39  37921  cdlemkfid1N  37926  cdlemkid1  37927  cdlemkid2  37929  cdlemkfid3N  37930  cdlemk19ylem  37935  cdlemk19xlem  37947  cdlemk19x  37948  cdlemk53b  37961  cdlemk53  37962  cdlemk54  37963  cdlemk55a  37964  cdlemk43N  37968  cdlemk19u1  37974  cdlemk19u  37975  cdleml1N  37981  erngdvlem4  37996  erngdvlem4-rN  38004  dia11N  38053  cdlemm10N  38123  dib11N  38165  cdlemn2  38200  cdlemn10  38211  dihjustlem  38221  dihord2cN  38226  dihlsscpre  38239  dih1dimb2  38246  dihvalcq2  38252  dihopelvalcpre  38253  dihord6b  38265  dih11  38270  dihmeetlem1N  38295  dihglblem2N  38299  dihglblem3N  38300  dihmeetlem2N  38304  dihglbcpreN  38305  dihmeetcN  38307  dihmeetbclemN  38309  dihmeetlem4preN  38311  dihmeetlem9N  38320  dihmeetlem20N  38331  dihlspsnssN  38337  dihlspsnat  38338  dihatlat  38339  dihglblem6  38345  dihmeet  38348  dochss  38370  hdmapval3N  38843  hgmap11  38907  nn0rppwr  39049  remulcand  39117  congtr  39429  fzmaxdif  39445  isnumbasgrplem2  39571  ntrclsk13  40288  ssmapsn  41346  infleinf  41507  suplesup2  41511  supxrunb3  41539  mullimc  41764  mullimcf  41771  islpcn  41787  limsupresxr  41914  liminfresxr  41915  cncfuni  42036  icccncfext  42037  stoweidlem34  42187  stoweidlem59  42212  stirlinglem13  42239  fourierdlem41  42301  fourierdlem42  42302  fourierdlem73  42332  sge0iunmptlemfi  42563  meadjiunlem  42615  ovncvrrp  42714  sssmf  42883  smflimsuplem7  42968  smflimsuplem8  42969  funressneu  43150  lincscm  44319  lincext3  44345  el0ldep  44355  el0ldepsnzr  44356  itscnhlc0xyqsol  44586
  Copyright terms: Public domain W3C validator