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  7238  eqfunresadj  7338  tfisi  7838  offsplitfpar  8101  poseq  8140  omeulem2  8550  uniinqs  8773  unxpdomlem3  9206  elfiun  9388  cantnffval  9623  tcrank  9844  cofsmo  10229  isfin2-2  10279  tskint  10745  tskun  10746  tskurn  10749  gruina  10778  dedekind  11344  subaddmulsub  11648  dmdcan  11899  lt2msq1  12074  supmullem1  12160  supmul  12162  xaddass  13216  xaddass2  13217  xlt2add  13227  xmulasslem3  13253  xadddi2r  13265  iccsplit  13453  expaddzlem  14077  expaddz  14078  expmulz  14080  ccatopth2  14689  pfxccat3  14706  resqrtcl  15226  limsupgle  15450  o1add  15587  o1mul  15588  o1sub  15589  bitsfzo  16412  sadfval  16429  smufval  16454  nn0rppwr  16538  prmexpb  16696  4sqlem18  16940  vdwlem10  16968  fsets  17146  setsstruct2  17151  submre  17573  mrelatlub  18528  gsmsymgreqlem2  19368  mndodcong  19479  subgabl  19773  gex2abl  19788  cntzsubrng  20483  cntzsubr  20522  abvres  20747  lbsind2  20995  lspsneu  21040  lbsextlem2  21076  lbsextg  21079  lindfind2  21734  matring  22337  maducoeval  22533  maducoeval2  22534  maduf  22535  madurid  22538  gsummatr01  22553  cramerimplem3  22579  cnprest  23183  hausnei2  23247  isreg2  23271  cmpcld  23296  llyrest  23379  nllyrest  23380  csdfil  23788  hausflimlem  23873  ssblps  24317  ssbl  24318  cphassi  25121  cphassir  25122  4cphipval2  25149  cphipval  25150  dvres2  25820  plyadd  26129  plymul  26130  coeeu  26137  vieta1  26227  aalioulem3  26249  aalioulem4  26250  efgh  26457  cxpadd  26595  cxpsub  26598  mulcxp  26601  divcxp  26603  cxple2  26613  cxplt2  26614  cxpcn3lem  26664  angcan  26719  ang180lem5  26730  isosctrlem3  26737  logexprlim  27143  lgssq  27255  abvcxp  27533  padicabv  27548  nosupbnd2lem1  27634  noinfbnd2lem1  27649  nosupinfsep  27651  noetalem1  27660  sltmul2  28081  brbtwn2  28839  ax5seglem6  28868  axcontlem4  28901  axcontlem8  28905  uhgr2edg  29142  nbgrisvtx  29275  nbupgrres  29298  clwwlkccat  29926  clwwlknonex2lem2  30044  frgrreggt1  30329  chscllem4  31576  cshwrnid  32890  ogrpinvlt  33044  ifscgr  36039  matunitlindflem1  37617  lshpnelb  38984  lfl1  39070  lshpkrlem6  39115  lshpkrex  39118  hlrelat3  39413  atbtwnexOLDN  39448  atbtwnex  39449  3dim3  39470  3atlem5  39488  2llnmat  39525  lvolex3N  39539  lvolnle3at  39583  4atlem11  39610  4atlem12  39613  dalemccea  39684  cdlema2N  39793  paddasslem2  39822  atmod1i1m  39859  lhp2lt  40002  lhp0lt  40004  lhpj1  40023  lhpmcvr4N  40027  lhpelim  40038  lhpmod2i2  40039  lhpmod6i1  40040  cdlemb2  40042  lhple  40043  lhpat  40044  4atex  40077  4atex2-0aOLDN  40079  4atex3  40082  ldilco  40117  ltrncl  40126  ltrn11  40127  ltrnle  40130  ltrncnvleN  40131  ltrnm  40132  ltrnj  40133  ltrncvr  40134  ltrnatb  40138  ltrnel  40140  ltrncnvel  40143  ltrncnv  40147  trlval2  40164  trlcnv  40166  trljat1  40167  trljat2  40168  trl0  40171  ltrnnidn  40175  trlnidatb  40178  cdlemc1  40192  cdlemc2  40193  cdlemc5  40196  cdlemc6  40197  cdlemd3  40201  cdlemd6  40204  cdleme0aa  40211  cdleme0b  40213  cdleme0c  40214  cdleme0e  40218  cdleme0fN  40219  cdleme01N  40222  cdleme02N  40223  cdleme0ex1N  40224  cdleme0moN  40226  cdleme3g  40235  cdleme3h  40236  cdleme3  40238  cdleme4  40239  cdleme4a  40240  cdleme5  40241  cdleme8  40251  cdleme9  40254  cdleme10  40255  cdleme16aN  40260  cdleme11a  40261  cdleme11fN  40265  cdleme11g  40266  cdleme11h  40267  cdleme11j  40268  cdleme11k  40269  cdleme12  40272  cdleme13  40273  cdleme17c  40289  cdleme17d1  40290  cdleme18a  40292  cdleme18b  40293  cdleme18c  40294  cdleme22gb  40295  cdlemeda  40299  cdlemednpq  40300  cdlemednuN  40301  cdleme19c  40306  cdleme20aN  40310  cdleme20bN  40311  cdleme20c  40312  cdleme22aa  40340  cdleme22a  40341  cdleme22b  40342  cdleme22d  40344  cdleme22e  40345  cdleme27cl  40367  cdleme27a  40368  cdleme30a  40379  cdleme42a  40472  cdleme42c  40473  cdleme50laut  40548  cdlemf1  40562  cdlemf  40564  cdlemfnid  40565  trlord  40570  cdlemg2fv2  40601  cdlemg2kq  40603  cdlemg2m  40605  cdlemg4a  40609  cdlemg4d  40614  cdlemg4g  40617  cdlemg4  40618  cdlemg6c  40621  cdlemg7aN  40626  cdlemg8a  40628  cdlemg8b  40629  cdlemg8c  40630  cdlemg9a  40633  cdlemg9b  40634  cdlemg9  40635  cdlemg11aq  40639  cdlemg10c  40640  cdlemg12a  40644  cdlemg12b  40645  cdlemg12c  40646  cdlemg17a  40662  cdlemg18b  40680  cdlemg18c  40681  cdlemg31b0a  40696  cdlemg31a  40698  cdlemg31b  40699  cdlemg31d  40701  cdlemg35  40714  trlcoabs2N  40723  trlcolem  40727  cdlemg44a  40732  trljco  40741  trljco2  40742  tendoco2  40769  tendopltp  40781  cdlemi1  40819  cdlemi2  40820  cdlemj3  40824  tendocan  40825  cdlemk3  40834  cdlemk4  40835  cdlemk5a  40836  cdlemk9  40840  cdlemk9bN  40841  cdlemkvcl  40843  cdlemk10  40844  cdlemk30  40895  cdlemk31  40897  cdlemk39  40917  cdlemkfid1N  40922  cdlemkid1  40923  cdlemkid2  40925  cdlemkfid3N  40926  cdlemk19ylem  40931  cdlemk19xlem  40943  cdlemk19x  40944  cdlemk53b  40957  cdlemk53  40958  cdlemk54  40959  cdlemk55a  40960  cdlemk43N  40964  cdlemk19u1  40970  cdlemk19u  40971  cdleml1N  40977  erngdvlem4  40992  erngdvlem4-rN  41000  dia11N  41049  cdlemm10N  41119  dib11N  41161  cdlemn2  41196  cdlemn10  41207  dihjustlem  41217  dihord2cN  41222  dihlsscpre  41235  dih1dimb2  41242  dihvalcq2  41248  dihopelvalcpre  41249  dihord6b  41261  dih11  41266  dihmeetlem1N  41291  dihglblem2N  41295  dihglblem3N  41296  dihmeetlem2N  41300  dihglbcpreN  41301  dihmeetcN  41303  dihmeetbclemN  41305  dihmeetlem4preN  41307  dihmeetlem9N  41316  dihmeetlem20N  41327  dihlspsnssN  41333  dihlspsnat  41334  dihatlat  41335  dihglblem6  41341  dihmeet  41344  dochss  41366  hdmapval3N  41839  hgmap11  41903  remulcand  42434  congtr  42961  fzmaxdif  42977  isnumbasgrplem2  43100  ntrclsk13  44067  ssmapsn  45217  infleinf  45375  suplesup2  45379  supxrunb3  45402  mullimc  45621  mullimcf  45628  islpcn  45644  limsupresxr  45771  liminfresxr  45772  cncfuni  45891  icccncfext  45892  stoweidlem34  46039  stoweidlem59  46064  stirlinglem13  46091  fourierdlem41  46153  fourierdlem42  46154  fourierdlem73  46184  sge0iunmptlemfi  46418  meadjiunlem  46470  ovncvrrp  46569  sssmf  46743  smflimsuplem7  46831  smflimsuplem8  46832  ormkglobd  46880  funressneu  47052  lincscm  48423  lincext3  48449  el0ldep  48459  el0ldepsnzr  48460  itscnhlc0xyqsol  48758  uptr2  49214