Theorem simp1l 1195

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 481	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)
2	1	3ad2ant1 1131	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 394   ∧ w3a 1085

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 206  df-an 395  df-3an 1087

This theorem is referenced by:  simp11l  1282  simp21l  1288  simp31l  1294  eqfunresadj  7359  tfisi  7850  offsplitfpar  8107  poseq  8146  omeulem2  8585  uniinqs  8793  unxpdomlem3  9254  elfiun  9427  cantnffval  9660  tcrank  9881  cofsmo  10266  isfin2-2  10316  tskint  10782  tskun  10783  tskurn  10786  gruina  10815  dedekind  11381  subaddmulsub  11681  dmdcan  11928  lt2msq1  12102  supmullem1  12188  supmul  12190  xaddass  13232  xaddass2  13233  xlt2add  13243  xmulasslem3  13269  xadddi2r  13281  iccsplit  13466  expaddzlem  14075  expaddz  14076  expmulz  14078  ccatopth2  14671  pfxccat3  14688  resqrtcl  15204  limsupgle  15425  o1add  15562  o1mul  15563  o1sub  15564  bitsfzo  16380  sadfval  16397  smufval  16422  prmexpb  16661  4sqlem18  16899  vdwlem10  16927  fsets  17106  setsstruct2  17111  submre  17553  mrelatlub  18519  gsmsymgreqlem2  19340  mndodcong  19451  subgabl  19745  gex2abl  19760  cntzsubrng  20455  cntzsubr  20496  abvres  20590  lbsind2  20836  lspsneu  20881  lbsextlem2  20917  lbsextg  20920  lindfind2  21592  matring  22165  maducoeval  22361  maducoeval2  22362  maduf  22363  madurid  22366  gsummatr01  22381  cramerimplem3  22407  cnprest  23013  hausnei2  23077  isreg2  23101  cmpcld  23126  llyrest  23209  nllyrest  23210  csdfil  23618  hausflimlem  23703  ssblps  24148  ssbl  24149  cphassi  24962  cphassir  24963  4cphipval2  24990  cphipval  24991  dvres2  25661  plyadd  25966  plymul  25967  coeeu  25974  vieta1  26061  aalioulem3  26083  aalioulem4  26084  efgh  26286  cxpadd  26423  cxpsub  26426  mulcxp  26429  divcxp  26431  cxple2  26441  cxplt2  26442  cxpcn3lem  26491  angcan  26543  ang180lem5  26554  isosctrlem3  26561  logexprlim  26964  lgssq  27076  abvcxp  27354  padicabv  27369  nosupbnd2lem1  27454  noinfbnd2lem1  27469  nosupinfsep  27471  noetalem1  27480  sltmul2  27862  brbtwn2  28430  ax5seglem6  28459  axcontlem4  28492  axcontlem8  28496  uhgr2edg  28732  nbgrisvtx  28865  nbupgrres  28888  clwwlkccat  29510  clwwlknonex2lem2  29628  frgrreggt1  29913  chscllem4  31160  cshwrnid  32392  ogrpinvlt  32511  ifscgr  35320  matunitlindflem1  36787  lshpnelb  38157  lfl1  38243  lshpkrlem6  38288  lshpkrex  38291  hlrelat3  38586  atbtwnexOLDN  38621  atbtwnex  38622  3dim3  38643  3atlem5  38661  2llnmat  38698  lvolex3N  38712  lvolnle3at  38756  4atlem11  38783  4atlem12  38786  dalemccea  38857  cdlema2N  38966  paddasslem2  38995  atmod1i1m  39032  lhp2lt  39175  lhp0lt  39177  lhpj1  39196  lhpmcvr4N  39200  lhpelim  39211  lhpmod2i2  39212  lhpmod6i1  39213  cdlemb2  39215  lhple  39216  lhpat  39217  4atex  39250  4atex2-0aOLDN  39252  4atex3  39255  ldilco  39290  ltrncl  39299  ltrn11  39300  ltrnle  39303  ltrncnvleN  39304  ltrnm  39305  ltrnj  39306  ltrncvr  39307  ltrnatb  39311  ltrnel  39313  ltrncnvel  39316  ltrncnv  39320  trlval2  39337  trlcnv  39339  trljat1  39340  trljat2  39341  trl0  39344  ltrnnidn  39348  trlnidatb  39351  cdlemc1  39365  cdlemc2  39366  cdlemc5  39369  cdlemc6  39370  cdlemd3  39374  cdlemd6  39377  cdleme0aa  39384  cdleme0b  39386  cdleme0c  39387  cdleme0e  39391  cdleme0fN  39392  cdleme01N  39395  cdleme02N  39396  cdleme0ex1N  39397  cdleme0moN  39399  cdleme3g  39408  cdleme3h  39409  cdleme3  39411  cdleme4  39412  cdleme4a  39413  cdleme5  39414  cdleme8  39424  cdleme9  39427  cdleme10  39428  cdleme16aN  39433  cdleme11a  39434  cdleme11fN  39438  cdleme11g  39439  cdleme11h  39440  cdleme11j  39441  cdleme11k  39442  cdleme12  39445  cdleme13  39446  cdleme17c  39462  cdleme17d1  39463  cdleme18a  39465  cdleme18b  39466  cdleme18c  39467  cdleme22gb  39468  cdlemeda  39472  cdlemednpq  39473  cdlemednuN  39474  cdleme19c  39479  cdleme20aN  39483  cdleme20bN  39484  cdleme20c  39485  cdleme22aa  39513  cdleme22a  39514  cdleme22b  39515  cdleme22d  39517  cdleme22e  39518  cdleme27cl  39540  cdleme27a  39541  cdleme30a  39552  cdleme42a  39645  cdleme42c  39646  cdleme50laut  39721  cdlemf1  39735  cdlemf  39737  cdlemfnid  39738  trlord  39743  cdlemg2fv2  39774  cdlemg2kq  39776  cdlemg2m  39778  cdlemg4a  39782  cdlemg4d  39787  cdlemg4g  39790  cdlemg4  39791  cdlemg6c  39794  cdlemg7aN  39799  cdlemg8a  39801  cdlemg8b  39802  cdlemg8c  39803  cdlemg9a  39806  cdlemg9b  39807  cdlemg9  39808  cdlemg11aq  39812  cdlemg10c  39813  cdlemg12a  39817  cdlemg12b  39818  cdlemg12c  39819  cdlemg17a  39835  cdlemg18b  39853  cdlemg18c  39854  cdlemg31b0a  39869  cdlemg31a  39871  cdlemg31b  39872  cdlemg31d  39874  cdlemg35  39887  trlcoabs2N  39896  trlcolem  39900  cdlemg44a  39905  trljco  39914  trljco2  39915  tendoco2  39942  tendopltp  39954  cdlemi1  39992  cdlemi2  39993  cdlemj3  39997  tendocan  39998  cdlemk3  40007  cdlemk4  40008  cdlemk5a  40009  cdlemk9  40013  cdlemk9bN  40014  cdlemkvcl  40016  cdlemk10  40017  cdlemk30  40068  cdlemk31  40070  cdlemk39  40090  cdlemkfid1N  40095  cdlemkid1  40096  cdlemkid2  40098  cdlemkfid3N  40099  cdlemk19ylem  40104  cdlemk19xlem  40116  cdlemk19x  40117  cdlemk53b  40130  cdlemk53  40131  cdlemk54  40132  cdlemk55a  40133  cdlemk43N  40137  cdlemk19u1  40143  cdlemk19u  40144  cdleml1N  40150  erngdvlem4  40165  erngdvlem4-rN  40173  dia11N  40222  cdlemm10N  40292  dib11N  40334  cdlemn2  40369  cdlemn10  40380  dihjustlem  40390  dihord2cN  40395  dihlsscpre  40408  dih1dimb2  40415  dihvalcq2  40421  dihopelvalcpre  40422  dihord6b  40434  dih11  40439  dihmeetlem1N  40464  dihglblem2N  40468  dihglblem3N  40469  dihmeetlem2N  40473  dihglbcpreN  40474  dihmeetcN  40476  dihmeetbclemN  40478  dihmeetlem4preN  40480  dihmeetlem9N  40489  dihmeetlem20N  40500  dihlspsnssN  40506  dihlspsnat  40507  dihatlat  40508  dihglblem6  40514  dihmeet  40517  dochss  40539  hdmapval3N  41012  hgmap11  41076  nn0rppwr  41526  remulcand  41613  congtr  42006  fzmaxdif  42022  isnumbasgrplem2  42148  ntrclsk13  43124  ssmapsn  44213  infleinf  44380  suplesup2  44384  supxrunb3  44407  mullimc  44630  mullimcf  44637  islpcn  44653  limsupresxr  44780  liminfresxr  44781  cncfuni  44900  icccncfext  44901  stoweidlem34  45048  stoweidlem59  45073  stirlinglem13  45100  fourierdlem41  45162  fourierdlem42  45163  fourierdlem73  45193  sge0iunmptlemfi  45427  meadjiunlem  45479  ovncvrrp  45578  sssmf  45752  smflimsuplem7  45840  smflimsuplem8  45841  funressneu  46055  lincscm  47198  lincext3  47224  el0ldep  47234  el0ldepsnzr  47235  itscnhlc0xyqsol  47538