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  7201  eqfunresadj  7301  tfisi  7799  offsplitfpar  8059  poseq  8098  omeulem2  8508  uniinqs  8731  unxpdomlem3  9157  elfiun  9339  cantnffval  9578  tcrank  9799  cofsmo  10182  isfin2-2  10232  tskint  10698  tskun  10699  tskurn  10702  gruina  10731  dedekind  11297  subaddmulsub  11601  dmdcan  11852  lt2msq1  12027  supmullem1  12113  supmul  12115  xaddass  13169  xaddass2  13170  xlt2add  13180  xmulasslem3  13206  xadddi2r  13218  iccsplit  13406  expaddzlem  14030  expaddz  14031  expmulz  14033  ccatopth2  14641  pfxccat3  14658  resqrtcl  15178  limsupgle  15402  o1add  15539  o1mul  15540  o1sub  15541  bitsfzo  16364  sadfval  16381  smufval  16406  nn0rppwr  16490  prmexpb  16648  4sqlem18  16892  vdwlem10  16920  fsets  17098  setsstruct2  17103  submre  17525  mrelatlub  18486  gsmsymgreqlem2  19328  mndodcong  19439  subgabl  19733  gex2abl  19748  ogrpinvlt  20041  cntzsubrng  20470  cntzsubr  20509  abvres  20734  lbsind2  21003  lspsneu  21048  lbsextlem2  21084  lbsextg  21087  lindfind2  21743  matring  22346  maducoeval  22542  maducoeval2  22543  maduf  22544  madurid  22547  gsummatr01  22562  cramerimplem3  22588  cnprest  23192  hausnei2  23256  isreg2  23280  cmpcld  23305  llyrest  23388  nllyrest  23389  csdfil  23797  hausflimlem  23882  ssblps  24326  ssbl  24327  cphassi  25130  cphassir  25131  4cphipval2  25158  cphipval  25159  dvres2  25829  plyadd  26138  plymul  26139  coeeu  26146  vieta1  26236  aalioulem3  26258  aalioulem4  26259  efgh  26466  cxpadd  26604  cxpsub  26607  mulcxp  26610  divcxp  26612  cxple2  26622  cxplt2  26623  cxpcn3lem  26673  angcan  26728  ang180lem5  26739  isosctrlem3  26746  logexprlim  27152  lgssq  27264  abvcxp  27542  padicabv  27557  nosupbnd2lem1  27643  noinfbnd2lem1  27658  nosupinfsep  27660  noetalem1  27669  sltmul2  28097  brbtwn2  28868  ax5seglem6  28897  axcontlem4  28930  axcontlem8  28934  uhgr2edg  29171  nbgrisvtx  29304  nbupgrres  29327  clwwlkccat  29952  clwwlknonex2lem2  30070  frgrreggt1  30355  chscllem4  31602  cshwrnid  32916  ifscgr  36017  matunitlindflem1  37595  lshpnelb  38962  lfl1  39048  lshpkrlem6  39093  lshpkrex  39096  hlrelat3  39391  atbtwnexOLDN  39426  atbtwnex  39427  3dim3  39448  3atlem5  39466  2llnmat  39503  lvolex3N  39517  lvolnle3at  39561  4atlem11  39588  4atlem12  39591  dalemccea  39662  cdlema2N  39771  paddasslem2  39800  atmod1i1m  39837  lhp2lt  39980  lhp0lt  39982  lhpj1  40001  lhpmcvr4N  40005  lhpelim  40016  lhpmod2i2  40017  lhpmod6i1  40018  cdlemb2  40020  lhple  40021  lhpat  40022  4atex  40055  4atex2-0aOLDN  40057  4atex3  40060  ldilco  40095  ltrncl  40104  ltrn11  40105  ltrnle  40108  ltrncnvleN  40109  ltrnm  40110  ltrnj  40111  ltrncvr  40112  ltrnatb  40116  ltrnel  40118  ltrncnvel  40121  ltrncnv  40125  trlval2  40142  trlcnv  40144  trljat1  40145  trljat2  40146  trl0  40149  ltrnnidn  40153  trlnidatb  40156  cdlemc1  40170  cdlemc2  40171  cdlemc5  40174  cdlemc6  40175  cdlemd3  40179  cdlemd6  40182  cdleme0aa  40189  cdleme0b  40191  cdleme0c  40192  cdleme0e  40196  cdleme0fN  40197  cdleme01N  40200  cdleme02N  40201  cdleme0ex1N  40202  cdleme0moN  40204  cdleme3g  40213  cdleme3h  40214  cdleme3  40216  cdleme4  40217  cdleme4a  40218  cdleme5  40219  cdleme8  40229  cdleme9  40232  cdleme10  40233  cdleme16aN  40238  cdleme11a  40239  cdleme11fN  40243  cdleme11g  40244  cdleme11h  40245  cdleme11j  40246  cdleme11k  40247  cdleme12  40250  cdleme13  40251  cdleme17c  40267  cdleme17d1  40268  cdleme18a  40270  cdleme18b  40271  cdleme18c  40272  cdleme22gb  40273  cdlemeda  40277  cdlemednpq  40278  cdlemednuN  40279  cdleme19c  40284  cdleme20aN  40288  cdleme20bN  40289  cdleme20c  40290  cdleme22aa  40318  cdleme22a  40319  cdleme22b  40320  cdleme22d  40322  cdleme22e  40323  cdleme27cl  40345  cdleme27a  40346  cdleme30a  40357  cdleme42a  40450  cdleme42c  40451  cdleme50laut  40526  cdlemf1  40540  cdlemf  40542  cdlemfnid  40543  trlord  40548  cdlemg2fv2  40579  cdlemg2kq  40581  cdlemg2m  40583  cdlemg4a  40587  cdlemg4d  40592  cdlemg4g  40595  cdlemg4  40596  cdlemg6c  40599  cdlemg7aN  40604  cdlemg8a  40606  cdlemg8b  40607  cdlemg8c  40608  cdlemg9a  40611  cdlemg9b  40612  cdlemg9  40613  cdlemg11aq  40617  cdlemg10c  40618  cdlemg12a  40622  cdlemg12b  40623  cdlemg12c  40624  cdlemg17a  40640  cdlemg18b  40658  cdlemg18c  40659  cdlemg31b0a  40674  cdlemg31a  40676  cdlemg31b  40677  cdlemg31d  40679  cdlemg35  40692  trlcoabs2N  40701  trlcolem  40705  cdlemg44a  40710  trljco  40719  trljco2  40720  tendoco2  40747  tendopltp  40759  cdlemi1  40797  cdlemi2  40798  cdlemj3  40802  tendocan  40803  cdlemk3  40812  cdlemk4  40813  cdlemk5a  40814  cdlemk9  40818  cdlemk9bN  40819  cdlemkvcl  40821  cdlemk10  40822  cdlemk30  40873  cdlemk31  40875  cdlemk39  40895  cdlemkfid1N  40900  cdlemkid1  40901  cdlemkid2  40903  cdlemkfid3N  40904  cdlemk19ylem  40909  cdlemk19xlem  40921  cdlemk19x  40922  cdlemk53b  40935  cdlemk53  40936  cdlemk54  40937  cdlemk55a  40938  cdlemk43N  40942  cdlemk19u1  40948  cdlemk19u  40949  cdleml1N  40955  erngdvlem4  40970  erngdvlem4-rN  40978  dia11N  41027  cdlemm10N  41097  dib11N  41139  cdlemn2  41174  cdlemn10  41185  dihjustlem  41195  dihord2cN  41200  dihlsscpre  41213  dih1dimb2  41220  dihvalcq2  41226  dihopelvalcpre  41227  dihord6b  41239  dih11  41244  dihmeetlem1N  41269  dihglblem2N  41273  dihglblem3N  41274  dihmeetlem2N  41278  dihglbcpreN  41279  dihmeetcN  41281  dihmeetbclemN  41283  dihmeetlem4preN  41285  dihmeetlem9N  41294  dihmeetlem20N  41305  dihlspsnssN  41311  dihlspsnat  41312  dihatlat  41313  dihglblem6  41319  dihmeet  41322  dochss  41344  hdmapval3N  41817  hgmap11  41881  remulcand  42412  congtr  42938  fzmaxdif  42954  isnumbasgrplem2  43077  ntrclsk13  44044  ssmapsn  45194  infleinf  45352  suplesup2  45356  supxrunb3  45379  mullimc  45598  mullimcf  45605  islpcn  45621  limsupresxr  45748  liminfresxr  45749  cncfuni  45868  icccncfext  45869  stoweidlem34  46016  stoweidlem59  46041  stirlinglem13  46068  fourierdlem41  46130  fourierdlem42  46131  fourierdlem73  46161  sge0iunmptlemfi  46395  meadjiunlem  46447  ovncvrrp  46546  sssmf  46720  smflimsuplem7  46808  smflimsuplem8  46809  ormkglobd  46857  funressneu  47032  grlimedgclnbgr  47980  lincscm  48416  lincext3  48442  el0ldep  48452  el0ldepsnzr  48453  itscnhlc0xyqsol  48751  uptr2  49207