Theorem simp1l 1078

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

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  simpl1l  1105  simpr1l  1111  simp11l  1165  simp21l  1171  simp31l  1177  funprgOLD  5855  tfisi  6950  omeulem2  7550  uniinqs  7714  unxpdomlem3  8051  elfiun  8219  cantnffval  8443  tcrank  8630  cofsmo  8974  isfin2-2  9024  tskint  9486  tskun  9487  tskurn  9490  gruina  9519  dedekind  10079  dmdcan  10614  lt2msq1  10786  supmullem1  10870  supmul  10872  xaddass  11951  xaddass2  11952  xlt2add  11962  xmulasslem3  11988  xadddi2r  12000  iccsplit  12176  expaddzlem  12765  expaddz  12766  expmulz  12768  ccatopth2  13323  swrdccat3  13343  resqrtcl  13842  limsupgle  14056  o1add  14192  o1mul  14193  o1sub  14194  bitsfzo  14995  sadfval  15012  smufval  15037  prmexpb  15268  4sqlem18  15504  vdwlem10  15532  fsets  15723  submre  16088  mrelatlub  17009  mndodcong  17784  subgabl  18064  gex2abl  18077  cntzsubr  18635  abvres  18662  lbsind2  18902  lspsneu  18944  lbsextlem2  18980  lbsextg  18983  lindfind2  19976  matring  20068  maducoeval  20264  maducoeval2  20265  maduf  20266  madurid  20269  gsummatr01  20284  cramerimplem3  20310  cnprest  20903  hausnei2  20967  isreg2  20991  cmpcld  21015  llyrest  21098  nllyrest  21099  csdfil  21508  hausflimlem  21593  ssblps  22037  ssbl  22038  cphassi  22822  cphassir  22823  4cphipval2  22849  cphipval  22850  dvres2  23482  plyadd  23777  plymul  23778  coeeu  23785  vieta1  23871  aalioulem3  23893  aalioulem4  23894  efgh  24091  cxpadd  24225  cxpsub  24228  mulcxp  24231  divcxp  24233  cxple2  24243  cxplt2  24244  cxpcn3lem  24288  angcan  24332  ang180lem5  24343  isosctrlem3  24350  logexprlim  24750  lgssq  24862  abvcxp  25104  padicabv  25119  brbtwn2  25585  ax5seglem6  25614  axcontlem4  25647  axcontlem8  25651  clwwlknimp  26304  chscllem4  27883  ogrpinvlt  29055  poseq  30994  wsuclemOLD  31018  nofulllem5  31105  ifscgr  31321  matunitlindflem1  32575  lshpnelb  33289  lfl1  33375  lshpkrlem6  33420  lshpkrex  33423  hlrelat3  33716  atbtwnexOLDN  33751  atbtwnex  33752  3dim3  33773  3atlem5  33791  2llnmat  33828  lvolex3N  33842  lvolnle3at  33886  4atlem11  33913  4atlem12  33916  dalemccea  33987  cdlema2N  34096  paddasslem2  34125  atmod1i1m  34162  lhp2lt  34305  lhp0lt  34307  lhpj1  34326  lhpmcvr4N  34330  lhpelim  34341  lhpmod2i2  34342  lhpmod6i1  34343  cdlemb2  34345  lhple  34346  lhpat  34347  4atex  34380  4atex2-0aOLDN  34382  4atex3  34385  ldilco  34420  ltrncl  34429  ltrn11  34430  ltrnle  34433  ltrncnvleN  34434  ltrnm  34435  ltrnj  34436  ltrncvr  34437  ltrnatb  34441  ltrnel  34443  ltrncnvel  34446  ltrncnv  34450  ltrnmwOLD  34456  trlval2  34468  trlcnv  34470  trljat1  34471  trljat2  34472  trl0  34475  ltrnnidn  34479  trlnidatb  34482  cdlemc1  34496  cdlemc2  34497  cdlemc5  34500  cdlemc6  34501  cdlemd3  34505  cdlemd6  34508  cdleme0aa  34515  cdleme0b  34517  cdleme0c  34518  cdleme0e  34522  cdleme0fN  34523  cdleme01N  34526  cdleme02N  34527  cdleme0ex1N  34528  cdleme0moN  34530  cdleme3g  34539  cdleme3h  34540  cdleme3  34542  cdleme4  34543  cdleme4a  34544  cdleme5  34545  cdleme8  34555  cdleme9  34558  cdleme10  34559  cdleme16aN  34564  cdleme11a  34565  cdleme11fN  34569  cdleme11g  34570  cdleme11h  34571  cdleme11j  34572  cdleme11k  34573  cdleme12  34576  cdleme13  34577  cdleme17c  34593  cdleme17d1  34594  cdleme18a  34596  cdleme18b  34597  cdleme18c  34598  cdleme22gb  34599  cdlemeda  34603  cdlemednpq  34604  cdlemednuN  34605  cdleme19c  34611  cdleme20aN  34615  cdleme20bN  34616  cdleme20c  34617  cdleme22aa  34645  cdleme22a  34646  cdleme22b  34647  cdleme22d  34649  cdleme22e  34650  cdleme27cl  34672  cdleme27a  34673  cdleme30a  34684  cdleme42a  34777  cdleme42c  34778  cdleme50laut  34853  cdlemf1  34867  cdlemf  34869  cdlemfnid  34870  trlord  34875  cdlemg2fv2  34906  cdlemg2kq  34908  cdlemg2m  34910  cdlemg4a  34914  cdlemg4d  34919  cdlemg4g  34922  cdlemg4  34923  cdlemg6c  34926  cdlemg7aN  34931  cdlemg8a  34933  cdlemg8b  34934  cdlemg8c  34935  cdlemg9a  34938  cdlemg9b  34939  cdlemg9  34940  cdlemg11aq  34944  cdlemg10c  34945  cdlemg12a  34949  cdlemg12b  34950  cdlemg12c  34951  cdlemg17a  34967  cdlemg18b  34985  cdlemg18c  34986  cdlemg31b0a  35001  cdlemg31a  35003  cdlemg31b  35004  cdlemg31d  35006  cdlemg35  35019  trlcoabs2N  35028  trlcolem  35032  cdlemg44a  35037  trljco  35046  trljco2  35047  tendoco2  35074  tendopltp  35086  cdlemi1  35124  cdlemi2  35125  cdlemj3  35129  tendocan  35130  cdlemk3  35139  cdlemk4  35140  cdlemk5a  35141  cdlemk9  35145  cdlemk9bN  35146  cdlemkvcl  35148  cdlemk10  35149  cdlemk30  35200  cdlemk31  35202  cdlemk39  35222  cdlemkfid1N  35227  cdlemkid1  35228  cdlemkid2  35230  cdlemkfid3N  35231  cdlemk19ylem  35236  cdlemk19xlem  35248  cdlemk19x  35249  cdlemk53b  35262  cdlemk53  35263  cdlemk54  35264  cdlemk55a  35265  cdlemk43N  35269  cdlemk19u1  35275  cdlemk19u  35276  cdleml1N  35282  erngdvlem4  35297  erngdvlem4-rN  35305  dia11N  35355  cdlemm10N  35425  dib11N  35467  cdlemn2  35502  cdlemn10  35513  dihjustlem  35523  dihord2cN  35528  dihlsscpre  35541  dih1dimb2  35548  dihvalcq2  35554  dihopelvalcpre  35555  dihord6b  35567  dih11  35572  dihmeetlem1N  35597  dihglblem2N  35601  dihglblem3N  35602  dihmeetlem2N  35606  dihglbcpreN  35607  dihmeetcN  35609  dihmeetbclemN  35611  dihmeetlem4preN  35613  dihmeetlem9N  35622  dihmeetlem20N  35633  dihlspsnssN  35639  dihlspsnat  35640  dihatlat  35641  dihglblem6  35647  dihmeet  35650  dochss  35672  hdmapval3N  36148  hgmap11  36212  congtr  36550  fzmaxdif  36566  isnumbasgrplem2  36693  ntrclsk13  37389  ssmapsn  38403  infleinf  38529  suplesup2  38533  mullimc  38683  mullimcf  38690  islpcn  38706  cncfuni  38772  icccncfext  38773  stoweidlem34  38927  stoweidlem59  38952  stirlinglem13  38979  fourierdlem41  39041  fourierdlem42  39042  fourierdlem73  39072  sge0iunmptlemfi  39306  meadjiunlem  39358  ovncvrrp  39454  sssmf  39625  pfxccat3  40289  uhgr2edg  40435  nbgrisvtx  40581  nbupgrres  40592  av-frgrareggt1  41547  lincscm  42013  lincext3  42039  el0ldep  42049  el0ldepsnzr  42050