Theorem simp1l 1198

Description: Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)

Assertion

Ref	Expression
simp1l	⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜑)

Proof of Theorem simp1l

Step	Hyp	Ref	Expression
1		simpl 482	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)
2	1	3ad2ant1 1133	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  simp11l  1285  simp21l  1291  simp31l  1297  2f1fvneq  7252  eqfunresadj  7352  tfisi  7852  offsplitfpar  8116  poseq  8155  omeulem2  8593  uniinqs  8809  unxpdomlem3  9258  elfiun  9440  cantnffval  9675  tcrank  9896  cofsmo  10281  isfin2-2  10331  tskint  10797  tskun  10798  tskurn  10801  gruina  10830  dedekind  11396  subaddmulsub  11698  dmdcan  11949  lt2msq1  12124  supmullem1  12210  supmul  12212  xaddass  13263  xaddass2  13264  xlt2add  13274  xmulasslem3  13300  xadddi2r  13312  iccsplit  13500  expaddzlem  14121  expaddz  14122  expmulz  14124  ccatopth2  14733  pfxccat3  14750  resqrtcl  15270  limsupgle  15491  o1add  15628  o1mul  15629  o1sub  15630  bitsfzo  16452  sadfval  16469  smufval  16494  nn0rppwr  16578  prmexpb  16736  4sqlem18  16980  vdwlem10  17008  fsets  17186  setsstruct2  17191  submre  17615  mrelatlub  18570  gsmsymgreqlem2  19410  mndodcong  19521  subgabl  19815  gex2abl  19830  cntzsubrng  20525  cntzsubr  20564  abvres  20789  lbsind2  21037  lspsneu  21082  lbsextlem2  21118  lbsextg  21121  lindfind2  21776  matring  22379  maducoeval  22575  maducoeval2  22576  maduf  22577  madurid  22580  gsummatr01  22595  cramerimplem3  22621  cnprest  23225  hausnei2  23289  isreg2  23313  cmpcld  23338  llyrest  23421  nllyrest  23422  csdfil  23830  hausflimlem  23915  ssblps  24359  ssbl  24360  cphassi  25164  cphassir  25165  4cphipval2  25192  cphipval  25193  dvres2  25863  plyadd  26172  plymul  26173  coeeu  26180  vieta1  26270  aalioulem3  26292  aalioulem4  26293  efgh  26500  cxpadd  26638  cxpsub  26641  mulcxp  26644  divcxp  26646  cxple2  26656  cxplt2  26657  cxpcn3lem  26707  angcan  26762  ang180lem5  26773  isosctrlem3  26780  logexprlim  27186  lgssq  27298  abvcxp  27576  padicabv  27591  nosupbnd2lem1  27677  noinfbnd2lem1  27692  nosupinfsep  27694  noetalem1  27703  sltmul2  28114  brbtwn2  28830  ax5seglem6  28859  axcontlem4  28892  axcontlem8  28896  uhgr2edg  29133  nbgrisvtx  29266  nbupgrres  29289  clwwlkccat  29917  clwwlknonex2lem2  30035  frgrreggt1  30320  chscllem4  31567  cshwrnid  32883  ogrpinvlt  33037  ifscgr  36008  matunitlindflem1  37586  lshpnelb  38948  lfl1  39034  lshpkrlem6  39079  lshpkrex  39082  hlrelat3  39377  atbtwnexOLDN  39412  atbtwnex  39413  3dim3  39434  3atlem5  39452  2llnmat  39489  lvolex3N  39503  lvolnle3at  39547  4atlem11  39574  4atlem12  39577  dalemccea  39648  cdlema2N  39757  paddasslem2  39786  atmod1i1m  39823  lhp2lt  39966  lhp0lt  39968  lhpj1  39987  lhpmcvr4N  39991  lhpelim  40002  lhpmod2i2  40003  lhpmod6i1  40004  cdlemb2  40006  lhple  40007  lhpat  40008  4atex  40041  4atex2-0aOLDN  40043  4atex3  40046  ldilco  40081  ltrncl  40090  ltrn11  40091  ltrnle  40094  ltrncnvleN  40095  ltrnm  40096  ltrnj  40097  ltrncvr  40098  ltrnatb  40102  ltrnel  40104  ltrncnvel  40107  ltrncnv  40111  trlval2  40128  trlcnv  40130  trljat1  40131  trljat2  40132  trl0  40135  ltrnnidn  40139  trlnidatb  40142  cdlemc1  40156  cdlemc2  40157  cdlemc5  40160  cdlemc6  40161  cdlemd3  40165  cdlemd6  40168  cdleme0aa  40175  cdleme0b  40177  cdleme0c  40178  cdleme0e  40182  cdleme0fN  40183  cdleme01N  40186  cdleme02N  40187  cdleme0ex1N  40188  cdleme0moN  40190  cdleme3g  40199  cdleme3h  40200  cdleme3  40202  cdleme4  40203  cdleme4a  40204  cdleme5  40205  cdleme8  40215  cdleme9  40218  cdleme10  40219  cdleme16aN  40224  cdleme11a  40225  cdleme11fN  40229  cdleme11g  40230  cdleme11h  40231  cdleme11j  40232  cdleme11k  40233  cdleme12  40236  cdleme13  40237  cdleme17c  40253  cdleme17d1  40254  cdleme18a  40256  cdleme18b  40257  cdleme18c  40258  cdleme22gb  40259  cdlemeda  40263  cdlemednpq  40264  cdlemednuN  40265  cdleme19c  40270  cdleme20aN  40274  cdleme20bN  40275  cdleme20c  40276  cdleme22aa  40304  cdleme22a  40305  cdleme22b  40306  cdleme22d  40308  cdleme22e  40309  cdleme27cl  40331  cdleme27a  40332  cdleme30a  40343  cdleme42a  40436  cdleme42c  40437  cdleme50laut  40512  cdlemf1  40526  cdlemf  40528  cdlemfnid  40529  trlord  40534  cdlemg2fv2  40565  cdlemg2kq  40567  cdlemg2m  40569  cdlemg4a  40573  cdlemg4d  40578  cdlemg4g  40581  cdlemg4  40582  cdlemg6c  40585  cdlemg7aN  40590  cdlemg8a  40592  cdlemg8b  40593  cdlemg8c  40594  cdlemg9a  40597  cdlemg9b  40598  cdlemg9  40599  cdlemg11aq  40603  cdlemg10c  40604  cdlemg12a  40608  cdlemg12b  40609  cdlemg12c  40610  cdlemg17a  40626  cdlemg18b  40644  cdlemg18c  40645  cdlemg31b0a  40660  cdlemg31a  40662  cdlemg31b  40663  cdlemg31d  40665  cdlemg35  40678  trlcoabs2N  40687  trlcolem  40691  cdlemg44a  40696  trljco  40705  trljco2  40706  tendoco2  40733  tendopltp  40745  cdlemi1  40783  cdlemi2  40784  cdlemj3  40788  tendocan  40789  cdlemk3  40798  cdlemk4  40799  cdlemk5a  40800  cdlemk9  40804  cdlemk9bN  40805  cdlemkvcl  40807  cdlemk10  40808  cdlemk30  40859  cdlemk31  40861  cdlemk39  40881  cdlemkfid1N  40886  cdlemkid1  40887  cdlemkid2  40889  cdlemkfid3N  40890  cdlemk19ylem  40895  cdlemk19xlem  40907  cdlemk19x  40908  cdlemk53b  40921  cdlemk53  40922  cdlemk54  40923  cdlemk55a  40924  cdlemk43N  40928  cdlemk19u1  40934  cdlemk19u  40935  cdleml1N  40941  erngdvlem4  40956  erngdvlem4-rN  40964  dia11N  41013  cdlemm10N  41083  dib11N  41125  cdlemn2  41160  cdlemn10  41171  dihjustlem  41181  dihord2cN  41186  dihlsscpre  41199  dih1dimb2  41206  dihvalcq2  41212  dihopelvalcpre  41213  dihord6b  41225  dih11  41230  dihmeetlem1N  41255  dihglblem2N  41259  dihglblem3N  41260  dihmeetlem2N  41264  dihglbcpreN  41265  dihmeetcN  41267  dihmeetbclemN  41269  dihmeetlem4preN  41271  dihmeetlem9N  41280  dihmeetlem20N  41291  dihlspsnssN  41297  dihlspsnat  41298  dihatlat  41299  dihglblem6  41305  dihmeet  41308  dochss  41330  hdmapval3N  41803  hgmap11  41867  remulcand  42428  congtr  42936  fzmaxdif  42952  isnumbasgrplem2  43075  ntrclsk13  44042  ssmapsn  45188  infleinf  45347  suplesup2  45351  supxrunb3  45374  mullimc  45593  mullimcf  45600  islpcn  45616  limsupresxr  45743  liminfresxr  45744  cncfuni  45863  icccncfext  45864  stoweidlem34  46011  stoweidlem59  46036  stirlinglem13  46063  fourierdlem41  46125  fourierdlem42  46126  fourierdlem73  46156  sge0iunmptlemfi  46390  meadjiunlem  46442  ovncvrrp  46541  sssmf  46715  smflimsuplem7  46803  smflimsuplem8  46804  ormkglobd  46852  funressneu  47024  lincscm  48354  lincext3  48380  el0ldep  48390  el0ldepsnzr  48391  itscnhlc0xyqsol  48693