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

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

Proof of Theorem simp1l
StepHypRef Expression
1 simpl 474 . 2 ((𝜑𝜓) → 𝜑)
213ad2ant1 1163 1 (((𝜑𝜓) ∧ 𝜒𝜃) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1107
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 198  df-an 385  df-3an 1109
This theorem is referenced by:  simpl1lOLD  1294  simpr1lOLD  1306  simp11l  1383  simp21l  1389  simp31l  1395  tfisi  7256  omeulem2  7868  uniinqs  8030  unxpdomlem3  8373  elfiun  8543  cantnffval  8775  tcrank  8962  cofsmo  9344  isfin2-2  9394  tskint  9860  tskun  9861  tskurn  9864  gruina  9893  dedekind  10454  dmdcan  10989  lt2msq1  11161  supmullem1  11247  supmul  11249  xaddass  12281  xaddass2  12282  xlt2add  12292  xmulasslem3  12318  xadddi2r  12330  iccsplit  12512  expaddzlem  13110  expaddz  13111  expmulz  13113  ccatopth2  13714  pfxccat3  13741  swrdccat3OLD  13742  resqrtcl  14279  limsupgle  14493  o1add  14629  o1mul  14630  o1sub  14631  bitsfzo  15438  sadfval  15455  smufval  15480  prmexpb  15709  4sqlem18  15945  vdwlem10  15973  fsets  16164  setsstruct2  16169  submre  16531  mrelatlub  17452  mndodcong  18225  subgabl  18507  gex2abl  18520  cntzsubr  19081  abvres  19108  lbsind2  19353  lspsneu  19395  lbsextlem2  19433  lbsextg  19436  lindfind2  20433  matring  20525  maducoeval  20722  maducoeval2  20723  maduf  20724  madurid  20727  gsummatr01  20743  cramerimplem3  20770  cnprest  21373  hausnei2  21437  isreg2  21461  cmpcld  21485  llyrest  21568  nllyrest  21569  csdfil  21977  hausflimlem  22062  ssblps  22506  ssbl  22507  cphassi  23292  cphassir  23293  4cphipval2  23319  cphipval  23320  dvres2  23967  plyadd  24264  plymul  24265  coeeu  24272  vieta1  24358  aalioulem3  24380  aalioulem4  24381  efgh  24579  cxpadd  24716  cxpsub  24719  mulcxp  24722  divcxp  24724  cxple2  24734  cxplt2  24735  cxpcn3lem  24779  angcan  24823  ang180lem5  24834  isosctrlem3  24841  logexprlim  25241  lgssq  25353  abvcxp  25595  padicabv  25610  brbtwn2  26076  ax5seglem6  26105  axcontlem4  26138  axcontlem8  26142  uhgr2edg  26378  nbgrisvtx  26514  nbgrisvtxOLD  26516  nbupgrres  26544  clwwlkccat  27217  frgrreggt1  27709  chscllem4  28955  ogrpinvlt  30171  eqfunresadj  32104  poseq  32197  nosupbnd2lem1  32305  noetalem5  32311  ifscgr  32595  matunitlindflem1  33829  lshpnelb  34940  lfl1  35026  lshpkrlem6  35071  lshpkrex  35074  hlrelat3  35368  atbtwnexOLDN  35403  atbtwnex  35404  3dim3  35425  3atlem5  35443  2llnmat  35480  lvolex3N  35494  lvolnle3at  35538  4atlem11  35565  4atlem12  35568  dalemccea  35639  cdlema2N  35748  paddasslem2  35777  atmod1i1m  35814  lhp2lt  35957  lhp0lt  35959  lhpj1  35978  lhpmcvr4N  35982  lhpelim  35993  lhpmod2i2  35994  lhpmod6i1  35995  cdlemb2  35997  lhple  35998  lhpat  35999  4atex  36032  4atex2-0aOLDN  36034  4atex3  36037  ldilco  36072  ltrncl  36081  ltrn11  36082  ltrnle  36085  ltrncnvleN  36086  ltrnm  36087  ltrnj  36088  ltrncvr  36089  ltrnatb  36093  ltrnel  36095  ltrncnvel  36098  ltrncnv  36102  trlval2  36119  trlcnv  36121  trljat1  36122  trljat2  36123  trl0  36126  ltrnnidn  36130  trlnidatb  36133  cdlemc1  36147  cdlemc2  36148  cdlemc5  36151  cdlemc6  36152  cdlemd3  36156  cdlemd6  36159  cdleme0aa  36166  cdleme0b  36168  cdleme0c  36169  cdleme0e  36173  cdleme0fN  36174  cdleme01N  36177  cdleme02N  36178  cdleme0ex1N  36179  cdleme0moN  36181  cdleme3g  36190  cdleme3h  36191  cdleme3  36193  cdleme4  36194  cdleme4a  36195  cdleme5  36196  cdleme8  36206  cdleme9  36209  cdleme10  36210  cdleme16aN  36215  cdleme11a  36216  cdleme11fN  36220  cdleme11g  36221  cdleme11h  36222  cdleme11j  36223  cdleme11k  36224  cdleme12  36227  cdleme13  36228  cdleme17c  36244  cdleme17d1  36245  cdleme18a  36247  cdleme18b  36248  cdleme18c  36249  cdleme22gb  36250  cdlemeda  36254  cdlemednpq  36255  cdlemednuN  36256  cdleme19c  36261  cdleme20aN  36265  cdleme20bN  36266  cdleme20c  36267  cdleme22aa  36295  cdleme22a  36296  cdleme22b  36297  cdleme22d  36299  cdleme22e  36300  cdleme27cl  36322  cdleme27a  36323  cdleme30a  36334  cdleme42a  36427  cdleme42c  36428  cdleme50laut  36503  cdlemf1  36517  cdlemf  36519  cdlemfnid  36520  trlord  36525  cdlemg2fv2  36556  cdlemg2kq  36558  cdlemg2m  36560  cdlemg4a  36564  cdlemg4d  36569  cdlemg4g  36572  cdlemg4  36573  cdlemg6c  36576  cdlemg7aN  36581  cdlemg8a  36583  cdlemg8b  36584  cdlemg8c  36585  cdlemg9a  36588  cdlemg9b  36589  cdlemg9  36590  cdlemg11aq  36594  cdlemg10c  36595  cdlemg12a  36599  cdlemg12b  36600  cdlemg12c  36601  cdlemg17a  36617  cdlemg18b  36635  cdlemg18c  36636  cdlemg31b0a  36651  cdlemg31a  36653  cdlemg31b  36654  cdlemg31d  36656  cdlemg35  36669  trlcoabs2N  36678  trlcolem  36682  cdlemg44a  36687  trljco  36696  trljco2  36697  tendoco2  36724  tendopltp  36736  cdlemi1  36774  cdlemi2  36775  cdlemj3  36779  tendocan  36780  cdlemk3  36789  cdlemk4  36790  cdlemk5a  36791  cdlemk9  36795  cdlemk9bN  36796  cdlemkvcl  36798  cdlemk10  36799  cdlemk30  36850  cdlemk31  36852  cdlemk39  36872  cdlemkfid1N  36877  cdlemkid1  36878  cdlemkid2  36880  cdlemkfid3N  36881  cdlemk19ylem  36886  cdlemk19xlem  36898  cdlemk19x  36899  cdlemk53b  36912  cdlemk53  36913  cdlemk54  36914  cdlemk55a  36915  cdlemk43N  36919  cdlemk19u1  36925  cdlemk19u  36926  cdleml1N  36932  erngdvlem4  36947  erngdvlem4-rN  36955  dia11N  37004  cdlemm10N  37074  dib11N  37116  cdlemn2  37151  cdlemn10  37162  dihjustlem  37172  dihord2cN  37177  dihlsscpre  37190  dih1dimb2  37197  dihvalcq2  37203  dihopelvalcpre  37204  dihord6b  37216  dih11  37221  dihmeetlem1N  37246  dihglblem2N  37250  dihglblem3N  37251  dihmeetlem2N  37255  dihglbcpreN  37256  dihmeetcN  37258  dihmeetbclemN  37260  dihmeetlem4preN  37262  dihmeetlem9N  37271  dihmeetlem20N  37282  dihlspsnssN  37288  dihlspsnat  37289  dihatlat  37290  dihglblem6  37296  dihmeet  37299  dochss  37321  hdmapval3N  37794  hgmap11  37858  congtr  38209  fzmaxdif  38225  isnumbasgrplem2  38351  ntrclsk13  39043  ssmapsn  40053  infleinf  40226  suplesup2  40230  supxrunb3  40260  mullimc  40486  mullimcf  40493  islpcn  40509  limsupresxr  40636  liminfresxr  40637  cncfuni  40737  icccncfext  40738  stoweidlem34  40888  stoweidlem59  40913  stirlinglem13  40940  fourierdlem41  41002  fourierdlem42  41003  fourierdlem73  41033  sge0iunmptlemfi  41267  meadjiunlem  41319  ovncvrrp  41418  sssmf  41587  smflimsuplem7  41672  smflimsuplem8  41673  funressneu  41825  lincscm  42888  lincext3  42914  el0ldep  42924  el0ldepsnzr  42925
  Copyright terms: Public domain W3C validator