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  7256  eqfunresadj  7362  tfisi  7859  offsplitfpar  8119  poseq  8159  omeulem2  8575  uniinqs  8802  unxpdomlem3  9233  elfiun  9406  cantnffval  9648  tcrank  9882  cofsmo  10328  isfin2-2  10378  tskint  10851  tskun  10852  tskurn  10855  gruina  10884  dedekind  11454  subaddmulsub  11760  dmdcan  12008  lt2msq1  12182  supmullem1  12268  supmul  12270  xaddass  13360  xaddass2  13361  xlt2add  13371  xmulasslem3  13397  xadddi2r  13409  iccsplit  13597  expaddzlem  14228  expaddz  14229  expmulz  14231  ccatopth2  14846  pfxccat3  14863  resqrtcl  15400  limsupgle  15624  o1add  15761  o1mul  15762  o1sub  15763  bitsfzo  16585  sadfval  16602  smufval  16627  nn0rppwr  16715  prmexpb  16875  4sqlem18  17120  vdwlem10  17148  fsets  17327  setsstruct2  17332  submre  17755  mrelatlub  18716  chnccat  18780  gsmsymgreqlem2  19625  mndodcong  19736  subgabl  20030  gex2abl  20045  ogrpinvlt  20338  rng1zrlem  20383  cntzsubrng  20799  cntzsubr  20838  abvres  21068  lbsind2  21336  lspsneu  21381  lbsextlem2  21417  lbsextg  21420  lindfind2  22104  matring  22738  maducoeval  22934  maducoeval2  22935  maduf  22936  madurid  22939  gsummatr01  22954  matunitlindflem1  22974  cramerimplem3  22983  cnprest  23587  hausnei2  23651  isreg2  23675  cmpcld  23700  llyrest  23784  nllyrest  23785  csdfil  24193  hausflimlem  24278  ssblps  24721  ssbl  24722  cphassi  25515  cphassir  25516  4cphipval2  25543  cphipval  25544  dvres2  26212  plyadd  26516  plymul  26517  coeeu  26524  vieta1  26617  aalioulem3  26643  aalioulem4  26644  efgh  26851  cxpadd  26989  cxpsub  26992  mulcxp  26995  divcxp  26997  cxple2  27007  cxplt2  27008  cxpcn3lem  27057  angcan  27112  ang180lem5  27123  isosctrlem3  27130  logexprlim  27534  lgssq  27646  abvcxp  27924  padicabv  27939  nosupbnd2lem1  28054  noinfbnd2lem1  28069  nosupinfsep  28071  noetalem1  28080  ltmuls2  28539  brbtwn2  29465  ax5seglem6  29494  axcontlem4  29527  axcontlem8  29531  uhgr2edg  29771  nbgrisvtx  29904  nbupgrres  29927  clwwlkccat  30563  clwwlknonex2lem2  30681  frgrreggt1  30976  chscllem4  32224  cshwrnid  33504  ifscgr  36779  lshpnelb  40009  lfl1  40095  lshpkrlem6  40140  lshpkrex  40143  hlrelat3  40437  atbtwnexOLDN  40472  atbtwnex  40473  3dim3  40494  3atlem5  40512  2llnmat  40549  lvolex3N  40563  lvolnle3at  40607  4atlem11  40634  4atlem12  40637  dalemccea  40708  cdlema2N  40817  paddasslem2  40846  atmod1i1m  40883  lhp2lt  41026  lhp0lt  41028  lhpj1  41047  lhpmcvr4N  41051  lhpelim  41062  lhpmod2i2  41063  lhpmod6i1  41064  cdlemb2  41066  lhple  41067  lhpat  41068  4atex  41101  4atex2-0aOLDN  41103  4atex3  41106  ldilco  41141  ltrncl  41150  ltrn11  41151  ltrnle  41154  ltrncnvleN  41155  ltrnm  41156  ltrnj  41157  ltrncvr  41158  ltrnatb  41162  ltrnel  41164  ltrncnvel  41167  ltrncnv  41171  trlval2  41188  trlcnv  41190  trljat1  41191  trljat2  41192  trl0  41195  ltrnnidn  41199  trlnidatb  41202  cdlemc1  41216  cdlemc2  41217  cdlemc5  41220  cdlemc6  41221  cdlemd3  41225  cdlemd6  41228  cdleme0aa  41235  cdleme0b  41237  cdleme0c  41238  cdleme0e  41242  cdleme0fN  41243  cdleme01N  41246  cdleme02N  41247  cdleme0ex1N  41248  cdleme0moN  41250  cdleme3g  41259  cdleme3h  41260  cdleme3  41262  cdleme4  41263  cdleme4a  41264  cdleme5  41265  cdleme8  41275  cdleme9  41278  cdleme10  41279  cdleme16aN  41284  cdleme11a  41285  cdleme11fN  41289  cdleme11g  41290  cdleme11h  41291  cdleme11j  41292  cdleme11k  41293  cdleme12  41296  cdleme13  41297  cdleme17c  41313  cdleme17d1  41314  cdleme18a  41316  cdleme18b  41317  cdleme18c  41318  cdleme22gb  41319  cdlemeda  41323  cdlemednpq  41324  cdlemednuN  41325  cdleme19c  41330  cdleme20aN  41334  cdleme20bN  41335  cdleme20c  41336  cdleme22aa  41364  cdleme22a  41365  cdleme22b  41366  cdleme22d  41368  cdleme22e  41369  cdleme27cl  41391  cdleme27a  41392  cdleme30a  41403  cdleme42a  41496  cdleme42c  41497  cdleme50laut  41572  cdlemf1  41586  cdlemf  41588  cdlemfnid  41589  trlord  41594  cdlemg2fv2  41625  cdlemg2kq  41627  cdlemg2m  41629  cdlemg4a  41633  cdlemg4d  41638  cdlemg4g  41641  cdlemg4  41642  cdlemg6c  41645  cdlemg7aN  41650  cdlemg8a  41652  cdlemg8b  41653  cdlemg8c  41654  cdlemg9a  41657  cdlemg9b  41658  cdlemg9  41659  cdlemg11aq  41663  cdlemg10c  41664  cdlemg12a  41668  cdlemg12b  41669  cdlemg12c  41670  cdlemg17a  41686  cdlemg18b  41704  cdlemg18c  41705  cdlemg31b0a  41720  cdlemg31a  41722  cdlemg31b  41723  cdlemg31d  41725  cdlemg35  41738  trlcoabs2N  41747  trlcolem  41751  cdlemg44a  41756  trljco  41765  trljco2  41766  tendoco2  41793  tendopltp  41805  cdlemi1  41843  cdlemi2  41844  cdlemj3  41848  tendocan  41849  cdlemk3  41858  cdlemk4  41859  cdlemk5a  41860  cdlemk9  41864  cdlemk9bN  41865  cdlemkvcl  41867  cdlemk10  41868  cdlemk30  41919  cdlemk31  41921  cdlemk39  41941  cdlemkfid1N  41946  cdlemkid1  41947  cdlemkid2  41949  cdlemkfid3N  41950  cdlemk19ylem  41955  cdlemk19xlem  41967  cdlemk19x  41968  cdlemk53b  41981  cdlemk53  41982  cdlemk54  41983  cdlemk55a  41984  cdlemk43N  41988  cdlemk19u1  41994  cdlemk19u  41995  cdleml1N  42001  erngdvlem4  42016  erngdvlem4-rN  42024  dia11N  42073  cdlemm10N  42143  dib11N  42185  cdlemn2  42220  cdlemn10  42231  dihjustlem  42241  dihord2cN  42246  dihlsscpre  42259  dih1dimb2  42266  dihvalcq2  42272  dihopelvalcpre  42273  dihord6b  42285  dih11  42290  dihmeetlem1N  42315  dihglblem2N  42319  dihglblem3N  42320  dihmeetlem2N  42324  dihglbcpreN  42325  dihmeetcN  42327  dihmeetbclemN  42329  dihmeetlem4preN  42331  dihmeetlem9N  42340  dihmeetlem20N  42351  dihlspsnssN  42357  dihlspsnat  42358  dihatlat  42359  dihglblem6  42365  dihmeet  42368  dochss  42390  hdmapval3N  42863  hgmap11  42927  remulcand  43458  congtr  43925  fzmaxdif  43941  isnumbasgrplem2  44064  ntrclsk13  45030  ssmapsn  46172  infleinf  46327  suplesup2  46331  supxrunb3  46354  mullimc  46572  mullimcf  46579  islpcn  46593  limsupresxr  46720  liminfresxr  46721  cncfuni  46840  icccncfext  46841  stoweidlem34  46988  stoweidlem59  47013  stirlinglem13  47040  fourierdlem41  47102  fourierdlem42  47103  fourierdlem73  47133  sge0iunmptlemfi  47367  meadjiunlem  47419  ovncvrrp  47518  sssmf  47692  smflimsuplem7  47780  smflimsuplem8  47781  ormkglobd  47831  funressneu  48061  grlimedgclnbgr  49037  lincscm  49486  lincext3  49512  el0ldep  49522  el0ldepsnzr  49523  itscnhlc0xyqsol  49821  uptr2  50273