Theorem simp1l 1199

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  1286  simp21l  1292  simp31l  1298  2f1fvneq  7216  eqfunresadj  7316  tfisi  7811  offsplitfpar  8071  poseq  8110  omeulem2  8520  uniinqs  8746  unxpdomlem3  9170  elfiun  9345  cantnffval  9584  tcrank  9808  cofsmo  10191  isfin2-2  10241  tskint  10708  tskun  10709  tskurn  10712  gruina  10741  dedekind  11308  subaddmulsub  11612  dmdcan  11863  lt2msq1  12038  supmullem1  12124  supmul  12126  xaddass  13176  xaddass2  13177  xlt2add  13187  xmulasslem3  13213  xadddi2r  13225  iccsplit  13413  expaddzlem  14040  expaddz  14041  expmulz  14043  ccatopth2  14652  pfxccat3  14669  resqrtcl  15188  limsupgle  15412  o1add  15549  o1mul  15550  o1sub  15551  bitsfzo  16374  sadfval  16391  smufval  16416  nn0rppwr  16500  prmexpb  16658  4sqlem18  16902  vdwlem10  16930  fsets  17108  setsstruct2  17113  submre  17536  mrelatlub  18497  chnccat  18561  gsmsymgreqlem2  19372  mndodcong  19483  subgabl  19777  gex2abl  19792  ogrpinvlt  20085  cntzsubrng  20512  cntzsubr  20551  abvres  20776  lbsind2  21045  lspsneu  21090  lbsextlem2  21126  lbsextg  21129  lindfind2  21785  matring  22399  maducoeval  22595  maducoeval2  22596  maduf  22597  madurid  22600  gsummatr01  22615  cramerimplem3  22641  cnprest  23245  hausnei2  23309  isreg2  23333  cmpcld  23358  llyrest  23441  nllyrest  23442  csdfil  23850  hausflimlem  23935  ssblps  24378  ssbl  24379  cphassi  25182  cphassir  25183  4cphipval2  25210  cphipval  25211  dvres2  25881  plyadd  26190  plymul  26191  coeeu  26198  vieta1  26288  aalioulem3  26310  aalioulem4  26311  efgh  26518  cxpadd  26656  cxpsub  26659  mulcxp  26662  divcxp  26664  cxple2  26674  cxplt2  26675  cxpcn3lem  26725  angcan  26780  ang180lem5  26791  isosctrlem3  26798  logexprlim  27204  lgssq  27316  abvcxp  27594  padicabv  27609  nosupbnd2lem1  27695  noinfbnd2lem1  27710  nosupinfsep  27712  noetalem1  27721  ltmuls2  28179  brbtwn2  28990  ax5seglem6  29019  axcontlem4  29052  axcontlem8  29056  uhgr2edg  29293  nbgrisvtx  29426  nbupgrres  29449  clwwlkccat  30077  clwwlknonex2lem2  30195  frgrreggt1  30480  chscllem4  31727  cshwrnid  33053  ifscgr  36257  matunitlindflem1  37861  lshpnelb  39354  lfl1  39440  lshpkrlem6  39485  lshpkrex  39488  hlrelat3  39782  atbtwnexOLDN  39817  atbtwnex  39818  3dim3  39839  3atlem5  39857  2llnmat  39894  lvolex3N  39908  lvolnle3at  39952  4atlem11  39979  4atlem12  39982  dalemccea  40053  cdlema2N  40162  paddasslem2  40191  atmod1i1m  40228  lhp2lt  40371  lhp0lt  40373  lhpj1  40392  lhpmcvr4N  40396  lhpelim  40407  lhpmod2i2  40408  lhpmod6i1  40409  cdlemb2  40411  lhple  40412  lhpat  40413  4atex  40446  4atex2-0aOLDN  40448  4atex3  40451  ldilco  40486  ltrncl  40495  ltrn11  40496  ltrnle  40499  ltrncnvleN  40500  ltrnm  40501  ltrnj  40502  ltrncvr  40503  ltrnatb  40507  ltrnel  40509  ltrncnvel  40512  ltrncnv  40516  trlval2  40533  trlcnv  40535  trljat1  40536  trljat2  40537  trl0  40540  ltrnnidn  40544  trlnidatb  40547  cdlemc1  40561  cdlemc2  40562  cdlemc5  40565  cdlemc6  40566  cdlemd3  40570  cdlemd6  40573  cdleme0aa  40580  cdleme0b  40582  cdleme0c  40583  cdleme0e  40587  cdleme0fN  40588  cdleme01N  40591  cdleme02N  40592  cdleme0ex1N  40593  cdleme0moN  40595  cdleme3g  40604  cdleme3h  40605  cdleme3  40607  cdleme4  40608  cdleme4a  40609  cdleme5  40610  cdleme8  40620  cdleme9  40623  cdleme10  40624  cdleme16aN  40629  cdleme11a  40630  cdleme11fN  40634  cdleme11g  40635  cdleme11h  40636  cdleme11j  40637  cdleme11k  40638  cdleme12  40641  cdleme13  40642  cdleme17c  40658  cdleme17d1  40659  cdleme18a  40661  cdleme18b  40662  cdleme18c  40663  cdleme22gb  40664  cdlemeda  40668  cdlemednpq  40669  cdlemednuN  40670  cdleme19c  40675  cdleme20aN  40679  cdleme20bN  40680  cdleme20c  40681  cdleme22aa  40709  cdleme22a  40710  cdleme22b  40711  cdleme22d  40713  cdleme22e  40714  cdleme27cl  40736  cdleme27a  40737  cdleme30a  40748  cdleme42a  40841  cdleme42c  40842  cdleme50laut  40917  cdlemf1  40931  cdlemf  40933  cdlemfnid  40934  trlord  40939  cdlemg2fv2  40970  cdlemg2kq  40972  cdlemg2m  40974  cdlemg4a  40978  cdlemg4d  40983  cdlemg4g  40986  cdlemg4  40987  cdlemg6c  40990  cdlemg7aN  40995  cdlemg8a  40997  cdlemg8b  40998  cdlemg8c  40999  cdlemg9a  41002  cdlemg9b  41003  cdlemg9  41004  cdlemg11aq  41008  cdlemg10c  41009  cdlemg12a  41013  cdlemg12b  41014  cdlemg12c  41015  cdlemg17a  41031  cdlemg18b  41049  cdlemg18c  41050  cdlemg31b0a  41065  cdlemg31a  41067  cdlemg31b  41068  cdlemg31d  41070  cdlemg35  41083  trlcoabs2N  41092  trlcolem  41096  cdlemg44a  41101  trljco  41110  trljco2  41111  tendoco2  41138  tendopltp  41150  cdlemi1  41188  cdlemi2  41189  cdlemj3  41193  tendocan  41194  cdlemk3  41203  cdlemk4  41204  cdlemk5a  41205  cdlemk9  41209  cdlemk9bN  41210  cdlemkvcl  41212  cdlemk10  41213  cdlemk30  41264  cdlemk31  41266  cdlemk39  41286  cdlemkfid1N  41291  cdlemkid1  41292  cdlemkid2  41294  cdlemkfid3N  41295  cdlemk19ylem  41300  cdlemk19xlem  41312  cdlemk19x  41313  cdlemk53b  41326  cdlemk53  41327  cdlemk54  41328  cdlemk55a  41329  cdlemk43N  41333  cdlemk19u1  41339  cdlemk19u  41340  cdleml1N  41346  erngdvlem4  41361  erngdvlem4-rN  41369  dia11N  41418  cdlemm10N  41488  dib11N  41530  cdlemn2  41565  cdlemn10  41576  dihjustlem  41586  dihord2cN  41591  dihlsscpre  41604  dih1dimb2  41611  dihvalcq2  41617  dihopelvalcpre  41618  dihord6b  41630  dih11  41635  dihmeetlem1N  41660  dihglblem2N  41664  dihglblem3N  41665  dihmeetlem2N  41669  dihglbcpreN  41670  dihmeetcN  41672  dihmeetbclemN  41674  dihmeetlem4preN  41676  dihmeetlem9N  41685  dihmeetlem20N  41696  dihlspsnssN  41702  dihlspsnat  41703  dihatlat  41704  dihglblem6  41710  dihmeet  41713  dochss  41735  hdmapval3N  42208  hgmap11  42272  remulcand  42803  congtr  43316  fzmaxdif  43332  isnumbasgrplem2  43455  ntrclsk13  44421  ssmapsn  45568  infleinf  45724  suplesup2  45728  supxrunb3  45751  mullimc  45970  mullimcf  45977  islpcn  45991  limsupresxr  46118  liminfresxr  46119  cncfuni  46238  icccncfext  46239  stoweidlem34  46386  stoweidlem59  46411  stirlinglem13  46438  fourierdlem41  46500  fourierdlem42  46501  fourierdlem73  46531  sge0iunmptlemfi  46765  meadjiunlem  46817  ovncvrrp  46916  sssmf  47090  smflimsuplem7  47178  smflimsuplem8  47179  ormkglobd  47227  funressneu  47401  grlimedgclnbgr  48349  lincscm  48784  lincext3  48810  el0ldep  48820  el0ldepsnzr  48821  itscnhlc0xyqsol  49119  uptr2  49574