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 1134	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 1089

This theorem is referenced by:  simp11l  1285  simp21l  1291  simp31l  1297  eqfunresadj  7380  tfisi  7880  offsplitfpar  8144  poseq  8183  omeulem2  8621  uniinqs  8837  unxpdomlem3  9288  elfiun  9470  cantnffval  9703  tcrank  9924  cofsmo  10309  isfin2-2  10359  tskint  10825  tskun  10826  tskurn  10829  gruina  10858  dedekind  11424  subaddmulsub  11726  dmdcan  11977  lt2msq1  12152  supmullem1  12238  supmul  12240  xaddass  13291  xaddass2  13292  xlt2add  13302  xmulasslem3  13328  xadddi2r  13340  iccsplit  13525  expaddzlem  14146  expaddz  14147  expmulz  14149  ccatopth2  14755  pfxccat3  14772  resqrtcl  15292  limsupgle  15513  o1add  15650  o1mul  15651  o1sub  15652  bitsfzo  16472  sadfval  16489  smufval  16514  nn0rppwr  16598  prmexpb  16756  4sqlem18  17000  vdwlem10  17028  fsets  17206  setsstruct2  17211  submre  17648  mrelatlub  18607  gsmsymgreqlem2  19449  mndodcong  19560  subgabl  19854  gex2abl  19869  cntzsubrng  20567  cntzsubr  20606  abvres  20832  lbsind2  21080  lspsneu  21125  lbsextlem2  21161  lbsextg  21164  lindfind2  21838  matring  22449  maducoeval  22645  maducoeval2  22646  maduf  22647  madurid  22650  gsummatr01  22665  cramerimplem3  22691  cnprest  23297  hausnei2  23361  isreg2  23385  cmpcld  23410  llyrest  23493  nllyrest  23494  csdfil  23902  hausflimlem  23987  ssblps  24432  ssbl  24433  cphassi  25248  cphassir  25249  4cphipval2  25276  cphipval  25277  dvres2  25947  plyadd  26256  plymul  26257  coeeu  26264  vieta1  26354  aalioulem3  26376  aalioulem4  26377  efgh  26583  cxpadd  26721  cxpsub  26724  mulcxp  26727  divcxp  26729  cxple2  26739  cxplt2  26740  cxpcn3lem  26790  angcan  26845  ang180lem5  26856  isosctrlem3  26863  logexprlim  27269  lgssq  27381  abvcxp  27659  padicabv  27674  nosupbnd2lem1  27760  noinfbnd2lem1  27775  nosupinfsep  27777  noetalem1  27786  sltmul2  28197  brbtwn2  28920  ax5seglem6  28949  axcontlem4  28982  axcontlem8  28986  uhgr2edg  29225  nbgrisvtx  29358  nbupgrres  29381  clwwlkccat  30009  clwwlknonex2lem2  30127  frgrreggt1  30412  chscllem4  31659  cshwrnid  32946  ogrpinvlt  33100  ifscgr  36045  matunitlindflem1  37623  lshpnelb  38985  lfl1  39071  lshpkrlem6  39116  lshpkrex  39119  hlrelat3  39414  atbtwnexOLDN  39449  atbtwnex  39450  3dim3  39471  3atlem5  39489  2llnmat  39526  lvolex3N  39540  lvolnle3at  39584  4atlem11  39611  4atlem12  39614  dalemccea  39685  cdlema2N  39794  paddasslem2  39823  atmod1i1m  39860  lhp2lt  40003  lhp0lt  40005  lhpj1  40024  lhpmcvr4N  40028  lhpelim  40039  lhpmod2i2  40040  lhpmod6i1  40041  cdlemb2  40043  lhple  40044  lhpat  40045  4atex  40078  4atex2-0aOLDN  40080  4atex3  40083  ldilco  40118  ltrncl  40127  ltrn11  40128  ltrnle  40131  ltrncnvleN  40132  ltrnm  40133  ltrnj  40134  ltrncvr  40135  ltrnatb  40139  ltrnel  40141  ltrncnvel  40144  ltrncnv  40148  trlval2  40165  trlcnv  40167  trljat1  40168  trljat2  40169  trl0  40172  ltrnnidn  40176  trlnidatb  40179  cdlemc1  40193  cdlemc2  40194  cdlemc5  40197  cdlemc6  40198  cdlemd3  40202  cdlemd6  40205  cdleme0aa  40212  cdleme0b  40214  cdleme0c  40215  cdleme0e  40219  cdleme0fN  40220  cdleme01N  40223  cdleme02N  40224  cdleme0ex1N  40225  cdleme0moN  40227  cdleme3g  40236  cdleme3h  40237  cdleme3  40239  cdleme4  40240  cdleme4a  40241  cdleme5  40242  cdleme8  40252  cdleme9  40255  cdleme10  40256  cdleme16aN  40261  cdleme11a  40262  cdleme11fN  40266  cdleme11g  40267  cdleme11h  40268  cdleme11j  40269  cdleme11k  40270  cdleme12  40273  cdleme13  40274  cdleme17c  40290  cdleme17d1  40291  cdleme18a  40293  cdleme18b  40294  cdleme18c  40295  cdleme22gb  40296  cdlemeda  40300  cdlemednpq  40301  cdlemednuN  40302  cdleme19c  40307  cdleme20aN  40311  cdleme20bN  40312  cdleme20c  40313  cdleme22aa  40341  cdleme22a  40342  cdleme22b  40343  cdleme22d  40345  cdleme22e  40346  cdleme27cl  40368  cdleme27a  40369  cdleme30a  40380  cdleme42a  40473  cdleme42c  40474  cdleme50laut  40549  cdlemf1  40563  cdlemf  40565  cdlemfnid  40566  trlord  40571  cdlemg2fv2  40602  cdlemg2kq  40604  cdlemg2m  40606  cdlemg4a  40610  cdlemg4d  40615  cdlemg4g  40618  cdlemg4  40619  cdlemg6c  40622  cdlemg7aN  40627  cdlemg8a  40629  cdlemg8b  40630  cdlemg8c  40631  cdlemg9a  40634  cdlemg9b  40635  cdlemg9  40636  cdlemg11aq  40640  cdlemg10c  40641  cdlemg12a  40645  cdlemg12b  40646  cdlemg12c  40647  cdlemg17a  40663  cdlemg18b  40681  cdlemg18c  40682  cdlemg31b0a  40697  cdlemg31a  40699  cdlemg31b  40700  cdlemg31d  40702  cdlemg35  40715  trlcoabs2N  40724  trlcolem  40728  cdlemg44a  40733  trljco  40742  trljco2  40743  tendoco2  40770  tendopltp  40782  cdlemi1  40820  cdlemi2  40821  cdlemj3  40825  tendocan  40826  cdlemk3  40835  cdlemk4  40836  cdlemk5a  40837  cdlemk9  40841  cdlemk9bN  40842  cdlemkvcl  40844  cdlemk10  40845  cdlemk30  40896  cdlemk31  40898  cdlemk39  40918  cdlemkfid1N  40923  cdlemkid1  40924  cdlemkid2  40926  cdlemkfid3N  40927  cdlemk19ylem  40932  cdlemk19xlem  40944  cdlemk19x  40945  cdlemk53b  40958  cdlemk53  40959  cdlemk54  40960  cdlemk55a  40961  cdlemk43N  40965  cdlemk19u1  40971  cdlemk19u  40972  cdleml1N  40978  erngdvlem4  40993  erngdvlem4-rN  41001  dia11N  41050  cdlemm10N  41120  dib11N  41162  cdlemn2  41197  cdlemn10  41208  dihjustlem  41218  dihord2cN  41223  dihlsscpre  41236  dih1dimb2  41243  dihvalcq2  41249  dihopelvalcpre  41250  dihord6b  41262  dih11  41267  dihmeetlem1N  41292  dihglblem2N  41296  dihglblem3N  41297  dihmeetlem2N  41301  dihglbcpreN  41302  dihmeetcN  41304  dihmeetbclemN  41306  dihmeetlem4preN  41308  dihmeetlem9N  41317  dihmeetlem20N  41328  dihlspsnssN  41334  dihlspsnat  41335  dihatlat  41336  dihglblem6  41342  dihmeet  41345  dochss  41367  hdmapval3N  41840  hgmap11  41904  remulcand  42468  congtr  42977  fzmaxdif  42993  isnumbasgrplem2  43116  ntrclsk13  44084  ssmapsn  45221  infleinf  45383  suplesup2  45387  supxrunb3  45410  mullimc  45631  mullimcf  45638  islpcn  45654  limsupresxr  45781  liminfresxr  45782  cncfuni  45901  icccncfext  45902  stoweidlem34  46049  stoweidlem59  46074  stirlinglem13  46101  fourierdlem41  46163  fourierdlem42  46164  fourierdlem73  46194  sge0iunmptlemfi  46428  meadjiunlem  46480  ovncvrrp  46579  sssmf  46753  smflimsuplem7  46841  smflimsuplem8  46842  ormkglobd  46890  funressneu  47059  lincscm  48347  lincext3  48373  el0ldep  48383  el0ldepsnzr  48384  itscnhlc0xyqsol  48686