Theorem simp1l 1193

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 485	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)
2	1	3ad2ant1 1129	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  simp11l  1280  simp21l  1286  simp31l  1292  tfisi  7567  offsplitfpar  7809  omeulem2  8203  uniinqs  8371  unxpdomlem3  8718  elfiun  8888  cantnffval  9120  tcrank  9307  cofsmo  9685  isfin2-2  9735  tskint  10201  tskun  10202  tskurn  10205  gruina  10234  dedekind  10797  subaddmulsub  11097  dmdcan  11344  lt2msq1  11518  supmullem1  11605  supmul  11607  xaddass  12636  xaddass2  12637  xlt2add  12647  xmulasslem3  12673  xadddi2r  12685  iccsplit  12865  expaddzlem  13466  expaddz  13467  expmulz  13469  ccatopth2  14073  pfxccat3  14090  resqrtcl  14607  limsupgle  14828  o1add  14964  o1mul  14965  o1sub  14966  bitsfzo  15778  sadfval  15795  smufval  15820  prmexpb  16056  4sqlem18  16292  vdwlem10  16320  fsets  16510  setsstruct2  16515  submre  16870  mrelatlub  17790  gsmsymgreqlem2  18553  mndodcong  18664  subgabl  18950  gex2abl  18965  cntzsubr  19562  abvres  19604  lbsind2  19847  lspsneu  19889  lbsextlem2  19925  lbsextg  19928  lindfind2  20956  matring  21046  maducoeval  21242  maducoeval2  21243  maduf  21244  madurid  21247  gsummatr01  21262  cramerimplem3  21288  cnprest  21891  hausnei2  21955  isreg2  21979  cmpcld  22004  llyrest  22087  nllyrest  22088  csdfil  22496  hausflimlem  22581  ssblps  23026  ssbl  23027  cphassi  23812  cphassir  23813  4cphipval2  23839  cphipval  23840  dvres2  24504  plyadd  24801  plymul  24802  coeeu  24809  vieta1  24895  aalioulem3  24917  aalioulem4  24918  efgh  25119  cxpadd  25256  cxpsub  25259  mulcxp  25262  divcxp  25264  cxple2  25274  cxplt2  25275  cxpcn3lem  25322  angcan  25374  ang180lem5  25385  isosctrlem3  25392  logexprlim  25795  lgssq  25907  abvcxp  26185  padicabv  26200  brbtwn2  26685  ax5seglem6  26714  axcontlem4  26747  axcontlem8  26751  uhgr2edg  26984  nbgrisvtx  27117  nbupgrres  27140  clwwlkccat  27762  clwwlknonex2lem2  27881  frgrreggt1  28166  chscllem4  29411  cshwrnid  30630  ogrpinvlt  30719  eqfunresadj  32999  poseq  33090  nosupbnd2lem1  33210  noetalem5  33216  ifscgr  33500  matunitlindflem1  34882  lshpnelb  36114  lfl1  36200  lshpkrlem6  36245  lshpkrex  36248  hlrelat3  36542  atbtwnexOLDN  36577  atbtwnex  36578  3dim3  36599  3atlem5  36617  2llnmat  36654  lvolex3N  36668  lvolnle3at  36712  4atlem11  36739  4atlem12  36742  dalemccea  36813  cdlema2N  36922  paddasslem2  36951  atmod1i1m  36988  lhp2lt  37131  lhp0lt  37133  lhpj1  37152  lhpmcvr4N  37156  lhpelim  37167  lhpmod2i2  37168  lhpmod6i1  37169  cdlemb2  37171  lhple  37172  lhpat  37173  4atex  37206  4atex2-0aOLDN  37208  4atex3  37211  ldilco  37246  ltrncl  37255  ltrn11  37256  ltrnle  37259  ltrncnvleN  37260  ltrnm  37261  ltrnj  37262  ltrncvr  37263  ltrnatb  37267  ltrnel  37269  ltrncnvel  37272  ltrncnv  37276  trlval2  37293  trlcnv  37295  trljat1  37296  trljat2  37297  trl0  37300  ltrnnidn  37304  trlnidatb  37307  cdlemc1  37321  cdlemc2  37322  cdlemc5  37325  cdlemc6  37326  cdlemd3  37330  cdlemd6  37333  cdleme0aa  37340  cdleme0b  37342  cdleme0c  37343  cdleme0e  37347  cdleme0fN  37348  cdleme01N  37351  cdleme02N  37352  cdleme0ex1N  37353  cdleme0moN  37355  cdleme3g  37364  cdleme3h  37365  cdleme3  37367  cdleme4  37368  cdleme4a  37369  cdleme5  37370  cdleme8  37380  cdleme9  37383  cdleme10  37384  cdleme16aN  37389  cdleme11a  37390  cdleme11fN  37394  cdleme11g  37395  cdleme11h  37396  cdleme11j  37397  cdleme11k  37398  cdleme12  37401  cdleme13  37402  cdleme17c  37418  cdleme17d1  37419  cdleme18a  37421  cdleme18b  37422  cdleme18c  37423  cdleme22gb  37424  cdlemeda  37428  cdlemednpq  37429  cdlemednuN  37430  cdleme19c  37435  cdleme20aN  37439  cdleme20bN  37440  cdleme20c  37441  cdleme22aa  37469  cdleme22a  37470  cdleme22b  37471  cdleme22d  37473  cdleme22e  37474  cdleme27cl  37496  cdleme27a  37497  cdleme30a  37508  cdleme42a  37601  cdleme42c  37602  cdleme50laut  37677  cdlemf1  37691  cdlemf  37693  cdlemfnid  37694  trlord  37699  cdlemg2fv2  37730  cdlemg2kq  37732  cdlemg2m  37734  cdlemg4a  37738  cdlemg4d  37743  cdlemg4g  37746  cdlemg4  37747  cdlemg6c  37750  cdlemg7aN  37755  cdlemg8a  37757  cdlemg8b  37758  cdlemg8c  37759  cdlemg9a  37762  cdlemg9b  37763  cdlemg9  37764  cdlemg11aq  37768  cdlemg10c  37769  cdlemg12a  37773  cdlemg12b  37774  cdlemg12c  37775  cdlemg17a  37791  cdlemg18b  37809  cdlemg18c  37810  cdlemg31b0a  37825  cdlemg31a  37827  cdlemg31b  37828  cdlemg31d  37830  cdlemg35  37843  trlcoabs2N  37852  trlcolem  37856  cdlemg44a  37861  trljco  37870  trljco2  37871  tendoco2  37898  tendopltp  37910  cdlemi1  37948  cdlemi2  37949  cdlemj3  37953  tendocan  37954  cdlemk3  37963  cdlemk4  37964  cdlemk5a  37965  cdlemk9  37969  cdlemk9bN  37970  cdlemkvcl  37972  cdlemk10  37973  cdlemk30  38024  cdlemk31  38026  cdlemk39  38046  cdlemkfid1N  38051  cdlemkid1  38052  cdlemkid2  38054  cdlemkfid3N  38055  cdlemk19ylem  38060  cdlemk19xlem  38072  cdlemk19x  38073  cdlemk53b  38086  cdlemk53  38087  cdlemk54  38088  cdlemk55a  38089  cdlemk43N  38093  cdlemk19u1  38099  cdlemk19u  38100  cdleml1N  38106  erngdvlem4  38121  erngdvlem4-rN  38129  dia11N  38178  cdlemm10N  38248  dib11N  38290  cdlemn2  38325  cdlemn10  38336  dihjustlem  38346  dihord2cN  38351  dihlsscpre  38364  dih1dimb2  38371  dihvalcq2  38377  dihopelvalcpre  38378  dihord6b  38390  dih11  38395  dihmeetlem1N  38420  dihglblem2N  38424  dihglblem3N  38425  dihmeetlem2N  38429  dihglbcpreN  38430  dihmeetcN  38432  dihmeetbclemN  38434  dihmeetlem4preN  38436  dihmeetlem9N  38445  dihmeetlem20N  38456  dihlspsnssN  38462  dihlspsnat  38463  dihatlat  38464  dihglblem6  38470  dihmeet  38473  dochss  38495  hdmapval3N  38968  hgmap11  39032  nn0rppwr  39175  remulcand  39243  congtr  39555  fzmaxdif  39571  isnumbasgrplem2  39697  ntrclsk13  40414  ssmapsn  41471  infleinf  41632  suplesup2  41636  supxrunb3  41664  mullimc  41889  mullimcf  41896  islpcn  41912  limsupresxr  42039  liminfresxr  42040  cncfuni  42161  icccncfext  42162  stoweidlem34  42312  stoweidlem59  42337  stirlinglem13  42364  fourierdlem41  42426  fourierdlem42  42427  fourierdlem73  42457  sge0iunmptlemfi  42688  meadjiunlem  42740  ovncvrrp  42839  sssmf  43008  smflimsuplem7  43093  smflimsuplem8  43094  funressneu  43275  lincscm  44478  lincext3  44504  el0ldep  44514  el0ldepsnzr  44515  itscnhlc0xyqsol  44745