Theorem simp1l 1196

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 1132	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  1283  simp21l  1289  simp31l  1295  eqfunresadj  7379  tfisi  7879  offsplitfpar  8142  poseq  8181  omeulem2  8619  uniinqs  8835  unxpdomlem3  9285  elfiun  9467  cantnffval  9700  tcrank  9921  cofsmo  10306  isfin2-2  10356  tskint  10822  tskun  10823  tskurn  10826  gruina  10855  dedekind  11421  subaddmulsub  11723  dmdcan  11974  lt2msq1  12149  supmullem1  12235  supmul  12237  xaddass  13287  xaddass2  13288  xlt2add  13298  xmulasslem3  13324  xadddi2r  13336  iccsplit  13521  expaddzlem  14142  expaddz  14143  expmulz  14145  ccatopth2  14751  pfxccat3  14768  resqrtcl  15288  limsupgle  15509  o1add  15646  o1mul  15647  o1sub  15648  bitsfzo  16468  sadfval  16485  smufval  16510  nn0rppwr  16594  prmexpb  16752  4sqlem18  16995  vdwlem10  17023  fsets  17202  setsstruct2  17207  submre  17649  mrelatlub  18619  gsmsymgreqlem2  19463  mndodcong  19574  subgabl  19868  gex2abl  19883  cntzsubrng  20583  cntzsubr  20622  abvres  20848  lbsind2  21097  lspsneu  21142  lbsextlem2  21178  lbsextg  21181  lindfind2  21855  matring  22464  maducoeval  22660  maducoeval2  22661  maduf  22662  madurid  22665  gsummatr01  22680  cramerimplem3  22706  cnprest  23312  hausnei2  23376  isreg2  23400  cmpcld  23425  llyrest  23508  nllyrest  23509  csdfil  23917  hausflimlem  24002  ssblps  24447  ssbl  24448  cphassi  25261  cphassir  25262  4cphipval2  25289  cphipval  25290  dvres2  25961  plyadd  26270  plymul  26271  coeeu  26278  vieta1  26368  aalioulem3  26390  aalioulem4  26391  efgh  26597  cxpadd  26735  cxpsub  26738  mulcxp  26741  divcxp  26743  cxple2  26753  cxplt2  26754  cxpcn3lem  26804  angcan  26859  ang180lem5  26870  isosctrlem3  26877  logexprlim  27283  lgssq  27395  abvcxp  27673  padicabv  27688  nosupbnd2lem1  27774  noinfbnd2lem1  27789  nosupinfsep  27791  noetalem1  27800  sltmul2  28211  brbtwn2  28934  ax5seglem6  28963  axcontlem4  28996  axcontlem8  29000  uhgr2edg  29239  nbgrisvtx  29372  nbupgrres  29395  clwwlkccat  30018  clwwlknonex2lem2  30136  frgrreggt1  30421  chscllem4  31668  cshwrnid  32930  ogrpinvlt  33082  ifscgr  36025  matunitlindflem1  37602  lshpnelb  38965  lfl1  39051  lshpkrlem6  39096  lshpkrex  39099  hlrelat3  39394  atbtwnexOLDN  39429  atbtwnex  39430  3dim3  39451  3atlem5  39469  2llnmat  39506  lvolex3N  39520  lvolnle3at  39564  4atlem11  39591  4atlem12  39594  dalemccea  39665  cdlema2N  39774  paddasslem2  39803  atmod1i1m  39840  lhp2lt  39983  lhp0lt  39985  lhpj1  40004  lhpmcvr4N  40008  lhpelim  40019  lhpmod2i2  40020  lhpmod6i1  40021  cdlemb2  40023  lhple  40024  lhpat  40025  4atex  40058  4atex2-0aOLDN  40060  4atex3  40063  ldilco  40098  ltrncl  40107  ltrn11  40108  ltrnle  40111  ltrncnvleN  40112  ltrnm  40113  ltrnj  40114  ltrncvr  40115  ltrnatb  40119  ltrnel  40121  ltrncnvel  40124  ltrncnv  40128  trlval2  40145  trlcnv  40147  trljat1  40148  trljat2  40149  trl0  40152  ltrnnidn  40156  trlnidatb  40159  cdlemc1  40173  cdlemc2  40174  cdlemc5  40177  cdlemc6  40178  cdlemd3  40182  cdlemd6  40185  cdleme0aa  40192  cdleme0b  40194  cdleme0c  40195  cdleme0e  40199  cdleme0fN  40200  cdleme01N  40203  cdleme02N  40204  cdleme0ex1N  40205  cdleme0moN  40207  cdleme3g  40216  cdleme3h  40217  cdleme3  40219  cdleme4  40220  cdleme4a  40221  cdleme5  40222  cdleme8  40232  cdleme9  40235  cdleme10  40236  cdleme16aN  40241  cdleme11a  40242  cdleme11fN  40246  cdleme11g  40247  cdleme11h  40248  cdleme11j  40249  cdleme11k  40250  cdleme12  40253  cdleme13  40254  cdleme17c  40270  cdleme17d1  40271  cdleme18a  40273  cdleme18b  40274  cdleme18c  40275  cdleme22gb  40276  cdlemeda  40280  cdlemednpq  40281  cdlemednuN  40282  cdleme19c  40287  cdleme20aN  40291  cdleme20bN  40292  cdleme20c  40293  cdleme22aa  40321  cdleme22a  40322  cdleme22b  40323  cdleme22d  40325  cdleme22e  40326  cdleme27cl  40348  cdleme27a  40349  cdleme30a  40360  cdleme42a  40453  cdleme42c  40454  cdleme50laut  40529  cdlemf1  40543  cdlemf  40545  cdlemfnid  40546  trlord  40551  cdlemg2fv2  40582  cdlemg2kq  40584  cdlemg2m  40586  cdlemg4a  40590  cdlemg4d  40595  cdlemg4g  40598  cdlemg4  40599  cdlemg6c  40602  cdlemg7aN  40607  cdlemg8a  40609  cdlemg8b  40610  cdlemg8c  40611  cdlemg9a  40614  cdlemg9b  40615  cdlemg9  40616  cdlemg11aq  40620  cdlemg10c  40621  cdlemg12a  40625  cdlemg12b  40626  cdlemg12c  40627  cdlemg17a  40643  cdlemg18b  40661  cdlemg18c  40662  cdlemg31b0a  40677  cdlemg31a  40679  cdlemg31b  40680  cdlemg31d  40682  cdlemg35  40695  trlcoabs2N  40704  trlcolem  40708  cdlemg44a  40713  trljco  40722  trljco2  40723  tendoco2  40750  tendopltp  40762  cdlemi1  40800  cdlemi2  40801  cdlemj3  40805  tendocan  40806  cdlemk3  40815  cdlemk4  40816  cdlemk5a  40817  cdlemk9  40821  cdlemk9bN  40822  cdlemkvcl  40824  cdlemk10  40825  cdlemk30  40876  cdlemk31  40878  cdlemk39  40898  cdlemkfid1N  40903  cdlemkid1  40904  cdlemkid2  40906  cdlemkfid3N  40907  cdlemk19ylem  40912  cdlemk19xlem  40924  cdlemk19x  40925  cdlemk53b  40938  cdlemk53  40939  cdlemk54  40940  cdlemk55a  40941  cdlemk43N  40945  cdlemk19u1  40951  cdlemk19u  40952  cdleml1N  40958  erngdvlem4  40973  erngdvlem4-rN  40981  dia11N  41030  cdlemm10N  41100  dib11N  41142  cdlemn2  41177  cdlemn10  41188  dihjustlem  41198  dihord2cN  41203  dihlsscpre  41216  dih1dimb2  41223  dihvalcq2  41229  dihopelvalcpre  41230  dihord6b  41242  dih11  41247  dihmeetlem1N  41272  dihglblem2N  41276  dihglblem3N  41277  dihmeetlem2N  41281  dihglbcpreN  41282  dihmeetcN  41284  dihmeetbclemN  41286  dihmeetlem4preN  41288  dihmeetlem9N  41297  dihmeetlem20N  41308  dihlspsnssN  41314  dihlspsnat  41315  dihatlat  41316  dihglblem6  41322  dihmeet  41325  dochss  41347  hdmapval3N  41820  hgmap11  41884  remulcand  42444  congtr  42953  fzmaxdif  42969  isnumbasgrplem2  43092  ntrclsk13  44060  ssmapsn  45158  infleinf  45321  suplesup2  45325  supxrunb3  45348  mullimc  45571  mullimcf  45578  islpcn  45594  limsupresxr  45721  liminfresxr  45722  cncfuni  45841  icccncfext  45842  stoweidlem34  45989  stoweidlem59  46014  stirlinglem13  46041  fourierdlem41  46103  fourierdlem42  46104  fourierdlem73  46134  sge0iunmptlemfi  46368  meadjiunlem  46420  ovncvrrp  46519  sssmf  46693  smflimsuplem7  46781  smflimsuplem8  46782  funressneu  46996  lincscm  48275  lincext3  48301  el0ldep  48311  el0ldepsnzr  48312  itscnhlc0xyqsol  48614