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 1133	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  1285  simp21l  1291  simp31l  1297  2f1fvneq  7200  eqfunresadj  7300  tfisi  7795  offsplitfpar  8055  poseq  8094  omeulem2  8504  uniinqs  8727  unxpdomlem3  9149  elfiun  9321  cantnffval  9560  tcrank  9784  cofsmo  10167  isfin2-2  10217  tskint  10683  tskun  10684  tskurn  10687  gruina  10716  dedekind  11283  subaddmulsub  11587  dmdcan  11838  lt2msq1  12013  supmullem1  12099  supmul  12101  xaddass  13150  xaddass2  13151  xlt2add  13161  xmulasslem3  13187  xadddi2r  13199  iccsplit  13387  expaddzlem  14014  expaddz  14015  expmulz  14017  ccatopth2  14626  pfxccat3  14643  resqrtcl  15162  limsupgle  15386  o1add  15523  o1mul  15524  o1sub  15525  bitsfzo  16348  sadfval  16365  smufval  16390  nn0rppwr  16474  prmexpb  16632  4sqlem18  16876  vdwlem10  16904  fsets  17082  setsstruct2  17087  submre  17509  mrelatlub  18470  chnccat  18534  gsmsymgreqlem2  19345  mndodcong  19456  subgabl  19750  gex2abl  19765  ogrpinvlt  20058  cntzsubrng  20484  cntzsubr  20523  abvres  20748  lbsind2  21017  lspsneu  21062  lbsextlem2  21098  lbsextg  21101  lindfind2  21757  matring  22359  maducoeval  22555  maducoeval2  22556  maduf  22557  madurid  22560  gsummatr01  22575  cramerimplem3  22601  cnprest  23205  hausnei2  23269  isreg2  23293  cmpcld  23318  llyrest  23401  nllyrest  23402  csdfil  23810  hausflimlem  23895  ssblps  24338  ssbl  24339  cphassi  25142  cphassir  25143  4cphipval2  25170  cphipval  25171  dvres2  25841  plyadd  26150  plymul  26151  coeeu  26158  vieta1  26248  aalioulem3  26270  aalioulem4  26271  efgh  26478  cxpadd  26616  cxpsub  26619  mulcxp  26622  divcxp  26624  cxple2  26634  cxplt2  26635  cxpcn3lem  26685  angcan  26740  ang180lem5  26751  isosctrlem3  26758  logexprlim  27164  lgssq  27276  abvcxp  27554  padicabv  27569  nosupbnd2lem1  27655  noinfbnd2lem1  27670  nosupinfsep  27672  noetalem1  27681  sltmul2  28111  brbtwn2  28885  ax5seglem6  28914  axcontlem4  28947  axcontlem8  28951  uhgr2edg  29188  nbgrisvtx  29321  nbupgrres  29344  clwwlkccat  29972  clwwlknonex2lem2  30090  frgrreggt1  30375  chscllem4  31622  cshwrnid  32949  ifscgr  36109  matunitlindflem1  37676  lshpnelb  39103  lfl1  39189  lshpkrlem6  39234  lshpkrex  39237  hlrelat3  39531  atbtwnexOLDN  39566  atbtwnex  39567  3dim3  39588  3atlem5  39606  2llnmat  39643  lvolex3N  39657  lvolnle3at  39701  4atlem11  39728  4atlem12  39731  dalemccea  39802  cdlema2N  39911  paddasslem2  39940  atmod1i1m  39977  lhp2lt  40120  lhp0lt  40122  lhpj1  40141  lhpmcvr4N  40145  lhpelim  40156  lhpmod2i2  40157  lhpmod6i1  40158  cdlemb2  40160  lhple  40161  lhpat  40162  4atex  40195  4atex2-0aOLDN  40197  4atex3  40200  ldilco  40235  ltrncl  40244  ltrn11  40245  ltrnle  40248  ltrncnvleN  40249  ltrnm  40250  ltrnj  40251  ltrncvr  40252  ltrnatb  40256  ltrnel  40258  ltrncnvel  40261  ltrncnv  40265  trlval2  40282  trlcnv  40284  trljat1  40285  trljat2  40286  trl0  40289  ltrnnidn  40293  trlnidatb  40296  cdlemc1  40310  cdlemc2  40311  cdlemc5  40314  cdlemc6  40315  cdlemd3  40319  cdlemd6  40322  cdleme0aa  40329  cdleme0b  40331  cdleme0c  40332  cdleme0e  40336  cdleme0fN  40337  cdleme01N  40340  cdleme02N  40341  cdleme0ex1N  40342  cdleme0moN  40344  cdleme3g  40353  cdleme3h  40354  cdleme3  40356  cdleme4  40357  cdleme4a  40358  cdleme5  40359  cdleme8  40369  cdleme9  40372  cdleme10  40373  cdleme16aN  40378  cdleme11a  40379  cdleme11fN  40383  cdleme11g  40384  cdleme11h  40385  cdleme11j  40386  cdleme11k  40387  cdleme12  40390  cdleme13  40391  cdleme17c  40407  cdleme17d1  40408  cdleme18a  40410  cdleme18b  40411  cdleme18c  40412  cdleme22gb  40413  cdlemeda  40417  cdlemednpq  40418  cdlemednuN  40419  cdleme19c  40424  cdleme20aN  40428  cdleme20bN  40429  cdleme20c  40430  cdleme22aa  40458  cdleme22a  40459  cdleme22b  40460  cdleme22d  40462  cdleme22e  40463  cdleme27cl  40485  cdleme27a  40486  cdleme30a  40497  cdleme42a  40590  cdleme42c  40591  cdleme50laut  40666  cdlemf1  40680  cdlemf  40682  cdlemfnid  40683  trlord  40688  cdlemg2fv2  40719  cdlemg2kq  40721  cdlemg2m  40723  cdlemg4a  40727  cdlemg4d  40732  cdlemg4g  40735  cdlemg4  40736  cdlemg6c  40739  cdlemg7aN  40744  cdlemg8a  40746  cdlemg8b  40747  cdlemg8c  40748  cdlemg9a  40751  cdlemg9b  40752  cdlemg9  40753  cdlemg11aq  40757  cdlemg10c  40758  cdlemg12a  40762  cdlemg12b  40763  cdlemg12c  40764  cdlemg17a  40780  cdlemg18b  40798  cdlemg18c  40799  cdlemg31b0a  40814  cdlemg31a  40816  cdlemg31b  40817  cdlemg31d  40819  cdlemg35  40832  trlcoabs2N  40841  trlcolem  40845  cdlemg44a  40850  trljco  40859  trljco2  40860  tendoco2  40887  tendopltp  40899  cdlemi1  40937  cdlemi2  40938  cdlemj3  40942  tendocan  40943  cdlemk3  40952  cdlemk4  40953  cdlemk5a  40954  cdlemk9  40958  cdlemk9bN  40959  cdlemkvcl  40961  cdlemk10  40962  cdlemk30  41013  cdlemk31  41015  cdlemk39  41035  cdlemkfid1N  41040  cdlemkid1  41041  cdlemkid2  41043  cdlemkfid3N  41044  cdlemk19ylem  41049  cdlemk19xlem  41061  cdlemk19x  41062  cdlemk53b  41075  cdlemk53  41076  cdlemk54  41077  cdlemk55a  41078  cdlemk43N  41082  cdlemk19u1  41088  cdlemk19u  41089  cdleml1N  41095  erngdvlem4  41110  erngdvlem4-rN  41118  dia11N  41167  cdlemm10N  41237  dib11N  41279  cdlemn2  41314  cdlemn10  41325  dihjustlem  41335  dihord2cN  41340  dihlsscpre  41353  dih1dimb2  41360  dihvalcq2  41366  dihopelvalcpre  41367  dihord6b  41379  dih11  41384  dihmeetlem1N  41409  dihglblem2N  41413  dihglblem3N  41414  dihmeetlem2N  41418  dihglbcpreN  41419  dihmeetcN  41421  dihmeetbclemN  41423  dihmeetlem4preN  41425  dihmeetlem9N  41434  dihmeetlem20N  41445  dihlspsnssN  41451  dihlspsnat  41452  dihatlat  41453  dihglblem6  41459  dihmeet  41462  dochss  41484  hdmapval3N  41957  hgmap11  42021  remulcand  42557  congtr  43082  fzmaxdif  43098  isnumbasgrplem2  43221  ntrclsk13  44188  ssmapsn  45337  infleinf  45494  suplesup2  45498  supxrunb3  45521  mullimc  45740  mullimcf  45747  islpcn  45761  limsupresxr  45888  liminfresxr  45889  cncfuni  46008  icccncfext  46009  stoweidlem34  46156  stoweidlem59  46181  stirlinglem13  46208  fourierdlem41  46270  fourierdlem42  46271  fourierdlem73  46301  sge0iunmptlemfi  46535  meadjiunlem  46587  ovncvrrp  46686  sssmf  46860  smflimsuplem7  46948  smflimsuplem8  46949  ormkglobd  46997  funressneu  47171  grlimedgclnbgr  48119  lincscm  48555  lincext3  48581  el0ldep  48591  el0ldepsnzr  48592  itscnhlc0xyqsol  48890  uptr2  49346