Theorem simp1l 1216

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  simp11l  1303  simp21l  1309  simp31l  1315  2f1fvneq  7261  eqfunresadj  7367  tfisi  7859  offsplitfpar  8120  poseq  8160  omeulem2  8574  uniinqs  8801  unxpdomlem3  9232  elfiun  9404  cantnffval  9646  tcrank  9870  cofsmo  10275  isfin2-2  10325  tskint  10798  tskun  10799  tskurn  10802  gruina  10831  dedekind  11401  subaddmulsub  11705  dmdcan  11953  lt2msq1  12127  supmullem1  12213  supmul  12215  xaddass  13305  xaddass2  13306  xlt2add  13316  xmulasslem3  13342  xadddi2r  13354  iccsplit  13542  expaddzlem  14173  expaddz  14174  expmulz  14176  ccatopth2  14790  pfxccat3  14807  resqrtcl  15344  limsupgle  15568  o1add  15705  o1mul  15706  o1sub  15707  bitsfzo  16531  sadfval  16548  smufval  16573  nn0rppwr  16657  prmexpb  16816  4sqlem18  17060  vdwlem10  17088  fsets  17267  setsstruct2  17272  submre  17695  mrelatlub  18656  chnccat  18720  gsmsymgreqlem2  19564  mndodcong  19675  subgabl  19969  gex2abl  19984  ogrpinvlt  20277  rng1zrlem  20322  cntzsubrng  20735  cntzsubr  20774  abvres  21003  lbsind2  21271  lspsneu  21316  lbsextlem2  21352  lbsextg  21355  lindfind2  22037  matring  22671  maducoeval  22867  maducoeval2  22868  maduf  22869  madurid  22872  gsummatr01  22887  matunitlindflem1  22907  cramerimplem3  22916  cnprest  23520  hausnei2  23584  isreg2  23608  cmpcld  23633  llyrest  23717  nllyrest  23718  csdfil  24126  hausflimlem  24211  ssblps  24654  ssbl  24655  cphassi  25448  cphassir  25449  4cphipval2  25476  cphipval  25477  dvres2  26146  plyadd  26450  plymul  26451  coeeu  26458  vieta1  26551  aalioulem3  26577  aalioulem4  26578  efgh  26786  cxpadd  26924  cxpsub  26927  mulcxp  26930  divcxp  26932  cxple2  26942  cxplt2  26943  cxpcn3lem  26992  angcan  27047  ang180lem5  27058  isosctrlem3  27065  logexprlim  27469  lgssq  27581  abvcxp  27859  padicabv  27874  nosupbnd2lem1  27959  noinfbnd2lem1  27974  nosupinfsep  27976  noetalem1  27985  ltmuls2  28444  brbtwn2  29370  ax5seglem6  29399  axcontlem4  29432  axcontlem8  29436  uhgr2edg  29676  nbgrisvtx  29809  nbupgrres  29832  clwwlkccat  30468  clwwlknonex2lem2  30586  frgrreggt1  30881  chscllem4  32129  cshwrnid  33409  ifscgr  36632  lshpnelb  39865  lfl1  39951  lshpkrlem6  39996  lshpkrex  39999  hlrelat3  40293  atbtwnexOLDN  40328  atbtwnex  40329  3dim3  40350  3atlem5  40368  2llnmat  40405  lvolex3N  40419  lvolnle3at  40463  4atlem11  40490  4atlem12  40493  dalemccea  40564  cdlema2N  40673  paddasslem2  40702  atmod1i1m  40739  lhp2lt  40882  lhp0lt  40884  lhpj1  40903  lhpmcvr4N  40907  lhpelim  40918  lhpmod2i2  40919  lhpmod6i1  40920  cdlemb2  40922  lhple  40923  lhpat  40924  4atex  40957  4atex2-0aOLDN  40959  4atex3  40962  ldilco  40997  ltrncl  41006  ltrn11  41007  ltrnle  41010  ltrncnvleN  41011  ltrnm  41012  ltrnj  41013  ltrncvr  41014  ltrnatb  41018  ltrnel  41020  ltrncnvel  41023  ltrncnv  41027  trlval2  41044  trlcnv  41046  trljat1  41047  trljat2  41048  trl0  41051  ltrnnidn  41055  trlnidatb  41058  cdlemc1  41072  cdlemc2  41073  cdlemc5  41076  cdlemc6  41077  cdlemd3  41081  cdlemd6  41084  cdleme0aa  41091  cdleme0b  41093  cdleme0c  41094  cdleme0e  41098  cdleme0fN  41099  cdleme01N  41102  cdleme02N  41103  cdleme0ex1N  41104  cdleme0moN  41106  cdleme3g  41115  cdleme3h  41116  cdleme3  41118  cdleme4  41119  cdleme4a  41120  cdleme5  41121  cdleme8  41131  cdleme9  41134  cdleme10  41135  cdleme16aN  41140  cdleme11a  41141  cdleme11fN  41145  cdleme11g  41146  cdleme11h  41147  cdleme11j  41148  cdleme11k  41149  cdleme12  41152  cdleme13  41153  cdleme17c  41169  cdleme17d1  41170  cdleme18a  41172  cdleme18b  41173  cdleme18c  41174  cdleme22gb  41175  cdlemeda  41179  cdlemednpq  41180  cdlemednuN  41181  cdleme19c  41186  cdleme20aN  41190  cdleme20bN  41191  cdleme20c  41192  cdleme22aa  41220  cdleme22a  41221  cdleme22b  41222  cdleme22d  41224  cdleme22e  41225  cdleme27cl  41247  cdleme27a  41248  cdleme30a  41259  cdleme42a  41352  cdleme42c  41353  cdleme50laut  41428  cdlemf1  41442  cdlemf  41444  cdlemfnid  41445  trlord  41450  cdlemg2fv2  41481  cdlemg2kq  41483  cdlemg2m  41485  cdlemg4a  41489  cdlemg4d  41494  cdlemg4g  41497  cdlemg4  41498  cdlemg6c  41501  cdlemg7aN  41506  cdlemg8a  41508  cdlemg8b  41509  cdlemg8c  41510  cdlemg9a  41513  cdlemg9b  41514  cdlemg9  41515  cdlemg11aq  41519  cdlemg10c  41520  cdlemg12a  41524  cdlemg12b  41525  cdlemg12c  41526  cdlemg17a  41542  cdlemg18b  41560  cdlemg18c  41561  cdlemg31b0a  41576  cdlemg31a  41578  cdlemg31b  41579  cdlemg31d  41581  cdlemg35  41594  trlcoabs2N  41603  trlcolem  41607  cdlemg44a  41612  trljco  41621  trljco2  41622  tendoco2  41649  tendopltp  41661  cdlemi1  41699  cdlemi2  41700  cdlemj3  41704  tendocan  41705  cdlemk3  41714  cdlemk4  41715  cdlemk5a  41716  cdlemk9  41720  cdlemk9bN  41721  cdlemkvcl  41723  cdlemk10  41724  cdlemk30  41775  cdlemk31  41777  cdlemk39  41797  cdlemkfid1N  41802  cdlemkid1  41803  cdlemkid2  41805  cdlemkfid3N  41806  cdlemk19ylem  41811  cdlemk19xlem  41823  cdlemk19x  41824  cdlemk53b  41837  cdlemk53  41838  cdlemk54  41839  cdlemk55a  41840  cdlemk43N  41844  cdlemk19u1  41850  cdlemk19u  41851  cdleml1N  41857  erngdvlem4  41872  erngdvlem4-rN  41880  dia11N  41929  cdlemm10N  41999  dib11N  42041  cdlemn2  42076  cdlemn10  42087  dihjustlem  42097  dihord2cN  42102  dihlsscpre  42115  dih1dimb2  42122  dihvalcq2  42128  dihopelvalcpre  42129  dihord6b  42141  dih11  42146  dihmeetlem1N  42171  dihglblem2N  42175  dihglblem3N  42176  dihmeetlem2N  42180  dihglbcpreN  42181  dihmeetcN  42183  dihmeetbclemN  42185  dihmeetlem4preN  42187  dihmeetlem9N  42196  dihmeetlem20N  42207  dihlspsnssN  42213  dihlspsnat  42214  dihatlat  42215  dihglblem6  42221  dihmeet  42224  dochss  42246  hdmapval3N  42719  hgmap11  42783  remulcand  43322  congtr  43814  fzmaxdif  43830  isnumbasgrplem2  43953  ntrclsk13  44919  ssmapsn  46054  infleinf  46209  suplesup2  46213  supxrunb3  46236  mullimc  46454  mullimcf  46461  islpcn  46475  limsupresxr  46602  liminfresxr  46603  cncfuni  46722  icccncfext  46723  stoweidlem34  46870  stoweidlem59  46895  stirlinglem13  46922  fourierdlem41  46984  fourierdlem42  46985  fourierdlem73  47015  sge0iunmptlemfi  47249  meadjiunlem  47301  ovncvrrp  47400  sssmf  47574  smflimsuplem7  47662  smflimsuplem8  47663  ormkglobd  47713  funressneu  47943  grlimedgclnbgr  48919  lincscm  49368  lincext3  49394  el0ldep  49404  el0ldepsnzr  49405  itscnhlc0xyqsol  49703  uptr2  50155