Theorem simp1l 1197

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 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  1284  simp21l  1290  simp31l  1296  eqfunresadj  7396  tfisi  7896  offsplitfpar  8160  poseq  8199  omeulem2  8639  uniinqs  8855  unxpdomlem3  9315  elfiun  9499  cantnffval  9732  tcrank  9953  cofsmo  10338  isfin2-2  10388  tskint  10854  tskun  10855  tskurn  10858  gruina  10887  dedekind  11453  subaddmulsub  11753  dmdcan  12004  lt2msq1  12179  supmullem1  12265  supmul  12267  xaddass  13311  xaddass2  13312  xlt2add  13322  xmulasslem3  13348  xadddi2r  13360  iccsplit  13545  expaddzlem  14156  expaddz  14157  expmulz  14159  ccatopth2  14765  pfxccat3  14782  resqrtcl  15302  limsupgle  15523  o1add  15660  o1mul  15661  o1sub  15662  bitsfzo  16481  sadfval  16498  smufval  16523  nn0rppwr  16608  prmexpb  16766  4sqlem18  17009  vdwlem10  17037  fsets  17216  setsstruct2  17221  submre  17663  mrelatlub  18632  gsmsymgreqlem2  19473  mndodcong  19584  subgabl  19878  gex2abl  19893  cntzsubrng  20593  cntzsubr  20634  abvres  20854  lbsind2  21103  lspsneu  21148  lbsextlem2  21184  lbsextg  21187  lindfind2  21861  matring  22470  maducoeval  22666  maducoeval2  22667  maduf  22668  madurid  22671  gsummatr01  22686  cramerimplem3  22712  cnprest  23318  hausnei2  23382  isreg2  23406  cmpcld  23431  llyrest  23514  nllyrest  23515  csdfil  23923  hausflimlem  24008  ssblps  24453  ssbl  24454  cphassi  25267  cphassir  25268  4cphipval2  25295  cphipval  25296  dvres2  25967  plyadd  26276  plymul  26277  coeeu  26284  vieta1  26372  aalioulem3  26394  aalioulem4  26395  efgh  26601  cxpadd  26739  cxpsub  26742  mulcxp  26745  divcxp  26747  cxple2  26757  cxplt2  26758  cxpcn3lem  26808  angcan  26863  ang180lem5  26874  isosctrlem3  26881  logexprlim  27287  lgssq  27399  abvcxp  27677  padicabv  27692  nosupbnd2lem1  27778  noinfbnd2lem1  27793  nosupinfsep  27795  noetalem1  27804  sltmul2  28215  brbtwn2  28938  ax5seglem6  28967  axcontlem4  29000  axcontlem8  29004  uhgr2edg  29243  nbgrisvtx  29376  nbupgrres  29399  clwwlkccat  30022  clwwlknonex2lem2  30140  frgrreggt1  30425  chscllem4  31672  cshwrnid  32928  ogrpinvlt  33073  ifscgr  36008  matunitlindflem1  37576  lshpnelb  38940  lfl1  39026  lshpkrlem6  39071  lshpkrex  39074  hlrelat3  39369  atbtwnexOLDN  39404  atbtwnex  39405  3dim3  39426  3atlem5  39444  2llnmat  39481  lvolex3N  39495  lvolnle3at  39539  4atlem11  39566  4atlem12  39569  dalemccea  39640  cdlema2N  39749  paddasslem2  39778  atmod1i1m  39815  lhp2lt  39958  lhp0lt  39960  lhpj1  39979  lhpmcvr4N  39983  lhpelim  39994  lhpmod2i2  39995  lhpmod6i1  39996  cdlemb2  39998  lhple  39999  lhpat  40000  4atex  40033  4atex2-0aOLDN  40035  4atex3  40038  ldilco  40073  ltrncl  40082  ltrn11  40083  ltrnle  40086  ltrncnvleN  40087  ltrnm  40088  ltrnj  40089  ltrncvr  40090  ltrnatb  40094  ltrnel  40096  ltrncnvel  40099  ltrncnv  40103  trlval2  40120  trlcnv  40122  trljat1  40123  trljat2  40124  trl0  40127  ltrnnidn  40131  trlnidatb  40134  cdlemc1  40148  cdlemc2  40149  cdlemc5  40152  cdlemc6  40153  cdlemd3  40157  cdlemd6  40160  cdleme0aa  40167  cdleme0b  40169  cdleme0c  40170  cdleme0e  40174  cdleme0fN  40175  cdleme01N  40178  cdleme02N  40179  cdleme0ex1N  40180  cdleme0moN  40182  cdleme3g  40191  cdleme3h  40192  cdleme3  40194  cdleme4  40195  cdleme4a  40196  cdleme5  40197  cdleme8  40207  cdleme9  40210  cdleme10  40211  cdleme16aN  40216  cdleme11a  40217  cdleme11fN  40221  cdleme11g  40222  cdleme11h  40223  cdleme11j  40224  cdleme11k  40225  cdleme12  40228  cdleme13  40229  cdleme17c  40245  cdleme17d1  40246  cdleme18a  40248  cdleme18b  40249  cdleme18c  40250  cdleme22gb  40251  cdlemeda  40255  cdlemednpq  40256  cdlemednuN  40257  cdleme19c  40262  cdleme20aN  40266  cdleme20bN  40267  cdleme20c  40268  cdleme22aa  40296  cdleme22a  40297  cdleme22b  40298  cdleme22d  40300  cdleme22e  40301  cdleme27cl  40323  cdleme27a  40324  cdleme30a  40335  cdleme42a  40428  cdleme42c  40429  cdleme50laut  40504  cdlemf1  40518  cdlemf  40520  cdlemfnid  40521  trlord  40526  cdlemg2fv2  40557  cdlemg2kq  40559  cdlemg2m  40561  cdlemg4a  40565  cdlemg4d  40570  cdlemg4g  40573  cdlemg4  40574  cdlemg6c  40577  cdlemg7aN  40582  cdlemg8a  40584  cdlemg8b  40585  cdlemg8c  40586  cdlemg9a  40589  cdlemg9b  40590  cdlemg9  40591  cdlemg11aq  40595  cdlemg10c  40596  cdlemg12a  40600  cdlemg12b  40601  cdlemg12c  40602  cdlemg17a  40618  cdlemg18b  40636  cdlemg18c  40637  cdlemg31b0a  40652  cdlemg31a  40654  cdlemg31b  40655  cdlemg31d  40657  cdlemg35  40670  trlcoabs2N  40679  trlcolem  40683  cdlemg44a  40688  trljco  40697  trljco2  40698  tendoco2  40725  tendopltp  40737  cdlemi1  40775  cdlemi2  40776  cdlemj3  40780  tendocan  40781  cdlemk3  40790  cdlemk4  40791  cdlemk5a  40792  cdlemk9  40796  cdlemk9bN  40797  cdlemkvcl  40799  cdlemk10  40800  cdlemk30  40851  cdlemk31  40853  cdlemk39  40873  cdlemkfid1N  40878  cdlemkid1  40879  cdlemkid2  40881  cdlemkfid3N  40882  cdlemk19ylem  40887  cdlemk19xlem  40899  cdlemk19x  40900  cdlemk53b  40913  cdlemk53  40914  cdlemk54  40915  cdlemk55a  40916  cdlemk43N  40920  cdlemk19u1  40926  cdlemk19u  40927  cdleml1N  40933  erngdvlem4  40948  erngdvlem4-rN  40956  dia11N  41005  cdlemm10N  41075  dib11N  41117  cdlemn2  41152  cdlemn10  41163  dihjustlem  41173  dihord2cN  41178  dihlsscpre  41191  dih1dimb2  41198  dihvalcq2  41204  dihopelvalcpre  41205  dihord6b  41217  dih11  41222  dihmeetlem1N  41247  dihglblem2N  41251  dihglblem3N  41252  dihmeetlem2N  41256  dihglbcpreN  41257  dihmeetcN  41259  dihmeetbclemN  41261  dihmeetlem4preN  41263  dihmeetlem9N  41272  dihmeetlem20N  41283  dihlspsnssN  41289  dihlspsnat  41290  dihatlat  41291  dihglblem6  41297  dihmeet  41300  dochss  41322  hdmapval3N  41795  hgmap11  41859  remulcand  42414  congtr  42922  fzmaxdif  42938  isnumbasgrplem2  43061  ntrclsk13  44033  ssmapsn  45123  infleinf  45287  suplesup2  45291  supxrunb3  45314  mullimc  45537  mullimcf  45544  islpcn  45560  limsupresxr  45687  liminfresxr  45688  cncfuni  45807  icccncfext  45808  stoweidlem34  45955  stoweidlem59  45980  stirlinglem13  46007  fourierdlem41  46069  fourierdlem42  46070  fourierdlem73  46100  sge0iunmptlemfi  46334  meadjiunlem  46386  ovncvrrp  46485  sssmf  46659  smflimsuplem7  46747  smflimsuplem8  46748  funressneu  46962  lincscm  48159  lincext3  48185  el0ldep  48195  el0ldepsnzr  48196  itscnhlc0xyqsol  48499