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  7206  eqfunresadj  7306  tfisi  7801  offsplitfpar  8061  poseq  8100  omeulem2  8510  uniinqs  8734  unxpdomlem3  9158  elfiun  9333  cantnffval  9572  tcrank  9796  cofsmo  10179  isfin2-2  10229  tskint  10696  tskun  10697  tskurn  10700  gruina  10729  dedekind  11296  subaddmulsub  11600  dmdcan  11851  lt2msq1  12026  supmullem1  12112  supmul  12114  xaddass  13164  xaddass2  13165  xlt2add  13175  xmulasslem3  13201  xadddi2r  13213  iccsplit  13401  expaddzlem  14028  expaddz  14029  expmulz  14031  ccatopth2  14640  pfxccat3  14657  resqrtcl  15176  limsupgle  15400  o1add  15537  o1mul  15538  o1sub  15539  bitsfzo  16362  sadfval  16379  smufval  16404  nn0rppwr  16488  prmexpb  16646  4sqlem18  16890  vdwlem10  16918  fsets  17096  setsstruct2  17101  submre  17524  mrelatlub  18485  chnccat  18549  gsmsymgreqlem2  19360  mndodcong  19471  subgabl  19765  gex2abl  19780  ogrpinvlt  20073  cntzsubrng  20500  cntzsubr  20539  abvres  20764  lbsind2  21033  lspsneu  21078  lbsextlem2  21114  lbsextg  21117  lindfind2  21773  matring  22387  maducoeval  22583  maducoeval2  22584  maduf  22585  madurid  22588  gsummatr01  22603  cramerimplem3  22629  cnprest  23233  hausnei2  23297  isreg2  23321  cmpcld  23346  llyrest  23429  nllyrest  23430  csdfil  23838  hausflimlem  23923  ssblps  24366  ssbl  24367  cphassi  25170  cphassir  25171  4cphipval2  25198  cphipval  25199  dvres2  25869  plyadd  26178  plymul  26179  coeeu  26186  vieta1  26276  aalioulem3  26298  aalioulem4  26299  efgh  26506  cxpadd  26644  cxpsub  26647  mulcxp  26650  divcxp  26652  cxple2  26662  cxplt2  26663  cxpcn3lem  26713  angcan  26768  ang180lem5  26779  isosctrlem3  26786  logexprlim  27192  lgssq  27304  abvcxp  27582  padicabv  27597  nosupbnd2lem1  27683  noinfbnd2lem1  27698  nosupinfsep  27700  noetalem1  27709  ltmuls2  28167  brbtwn2  28978  ax5seglem6  29007  axcontlem4  29040  axcontlem8  29044  uhgr2edg  29281  nbgrisvtx  29414  nbupgrres  29437  clwwlkccat  30065  clwwlknonex2lem2  30183  frgrreggt1  30468  chscllem4  31715  cshwrnid  33043  ifscgr  36238  matunitlindflem1  37813  lshpnelb  39240  lfl1  39326  lshpkrlem6  39371  lshpkrex  39374  hlrelat3  39668  atbtwnexOLDN  39703  atbtwnex  39704  3dim3  39725  3atlem5  39743  2llnmat  39780  lvolex3N  39794  lvolnle3at  39838  4atlem11  39865  4atlem12  39868  dalemccea  39939  cdlema2N  40048  paddasslem2  40077  atmod1i1m  40114  lhp2lt  40257  lhp0lt  40259  lhpj1  40278  lhpmcvr4N  40282  lhpelim  40293  lhpmod2i2  40294  lhpmod6i1  40295  cdlemb2  40297  lhple  40298  lhpat  40299  4atex  40332  4atex2-0aOLDN  40334  4atex3  40337  ldilco  40372  ltrncl  40381  ltrn11  40382  ltrnle  40385  ltrncnvleN  40386  ltrnm  40387  ltrnj  40388  ltrncvr  40389  ltrnatb  40393  ltrnel  40395  ltrncnvel  40398  ltrncnv  40402  trlval2  40419  trlcnv  40421  trljat1  40422  trljat2  40423  trl0  40426  ltrnnidn  40430  trlnidatb  40433  cdlemc1  40447  cdlemc2  40448  cdlemc5  40451  cdlemc6  40452  cdlemd3  40456  cdlemd6  40459  cdleme0aa  40466  cdleme0b  40468  cdleme0c  40469  cdleme0e  40473  cdleme0fN  40474  cdleme01N  40477  cdleme02N  40478  cdleme0ex1N  40479  cdleme0moN  40481  cdleme3g  40490  cdleme3h  40491  cdleme3  40493  cdleme4  40494  cdleme4a  40495  cdleme5  40496  cdleme8  40506  cdleme9  40509  cdleme10  40510  cdleme16aN  40515  cdleme11a  40516  cdleme11fN  40520  cdleme11g  40521  cdleme11h  40522  cdleme11j  40523  cdleme11k  40524  cdleme12  40527  cdleme13  40528  cdleme17c  40544  cdleme17d1  40545  cdleme18a  40547  cdleme18b  40548  cdleme18c  40549  cdleme22gb  40550  cdlemeda  40554  cdlemednpq  40555  cdlemednuN  40556  cdleme19c  40561  cdleme20aN  40565  cdleme20bN  40566  cdleme20c  40567  cdleme22aa  40595  cdleme22a  40596  cdleme22b  40597  cdleme22d  40599  cdleme22e  40600  cdleme27cl  40622  cdleme27a  40623  cdleme30a  40634  cdleme42a  40727  cdleme42c  40728  cdleme50laut  40803  cdlemf1  40817  cdlemf  40819  cdlemfnid  40820  trlord  40825  cdlemg2fv2  40856  cdlemg2kq  40858  cdlemg2m  40860  cdlemg4a  40864  cdlemg4d  40869  cdlemg4g  40872  cdlemg4  40873  cdlemg6c  40876  cdlemg7aN  40881  cdlemg8a  40883  cdlemg8b  40884  cdlemg8c  40885  cdlemg9a  40888  cdlemg9b  40889  cdlemg9  40890  cdlemg11aq  40894  cdlemg10c  40895  cdlemg12a  40899  cdlemg12b  40900  cdlemg12c  40901  cdlemg17a  40917  cdlemg18b  40935  cdlemg18c  40936  cdlemg31b0a  40951  cdlemg31a  40953  cdlemg31b  40954  cdlemg31d  40956  cdlemg35  40969  trlcoabs2N  40978  trlcolem  40982  cdlemg44a  40987  trljco  40996  trljco2  40997  tendoco2  41024  tendopltp  41036  cdlemi1  41074  cdlemi2  41075  cdlemj3  41079  tendocan  41080  cdlemk3  41089  cdlemk4  41090  cdlemk5a  41091  cdlemk9  41095  cdlemk9bN  41096  cdlemkvcl  41098  cdlemk10  41099  cdlemk30  41150  cdlemk31  41152  cdlemk39  41172  cdlemkfid1N  41177  cdlemkid1  41178  cdlemkid2  41180  cdlemkfid3N  41181  cdlemk19ylem  41186  cdlemk19xlem  41198  cdlemk19x  41199  cdlemk53b  41212  cdlemk53  41213  cdlemk54  41214  cdlemk55a  41215  cdlemk43N  41219  cdlemk19u1  41225  cdlemk19u  41226  cdleml1N  41232  erngdvlem4  41247  erngdvlem4-rN  41255  dia11N  41304  cdlemm10N  41374  dib11N  41416  cdlemn2  41451  cdlemn10  41462  dihjustlem  41472  dihord2cN  41477  dihlsscpre  41490  dih1dimb2  41497  dihvalcq2  41503  dihopelvalcpre  41504  dihord6b  41516  dih11  41521  dihmeetlem1N  41546  dihglblem2N  41550  dihglblem3N  41551  dihmeetlem2N  41555  dihglbcpreN  41556  dihmeetcN  41558  dihmeetbclemN  41560  dihmeetlem4preN  41562  dihmeetlem9N  41571  dihmeetlem20N  41582  dihlspsnssN  41588  dihlspsnat  41589  dihatlat  41590  dihglblem6  41596  dihmeet  41599  dochss  41621  hdmapval3N  42094  hgmap11  42158  remulcand  42690  congtr  43203  fzmaxdif  43219  isnumbasgrplem2  43342  ntrclsk13  44308  ssmapsn  45456  infleinf  45612  suplesup2  45616  supxrunb3  45639  mullimc  45858  mullimcf  45865  islpcn  45879  limsupresxr  46006  liminfresxr  46007  cncfuni  46126  icccncfext  46127  stoweidlem34  46274  stoweidlem59  46299  stirlinglem13  46326  fourierdlem41  46388  fourierdlem42  46389  fourierdlem73  46419  sge0iunmptlemfi  46653  meadjiunlem  46705  ovncvrrp  46804  sssmf  46978  smflimsuplem7  47066  smflimsuplem8  47067  ormkglobd  47115  funressneu  47289  grlimedgclnbgr  48237  lincscm  48672  lincext3  48698  el0ldep  48708  el0ldepsnzr  48709  itscnhlc0xyqsol  49007  uptr2  49462