Theorem simp1l 1216

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  simp11l  1303  simp21l  1309  simp31l  1315  2f1fvneq  7265  eqfunresadj  7371  tfisi  7864  offsplitfpar  8123  poseq  8163  omeulem2  8577  uniinqs  8804  unxpdomlem3  9228  elfiun  9400  cantnffval  9642  tcrank  9866  cofsmo  10271  isfin2-2  10321  tskint  10788  tskun  10789  tskurn  10792  gruina  10821  dedekind  11391  subaddmulsub  11695  dmdcan  11943  lt2msq1  12117  supmullem1  12203  supmul  12205  xaddass  13293  xaddass2  13294  xlt2add  13304  xmulasslem3  13330  xadddi2r  13342  iccsplit  13530  expaddzlem  14161  expaddz  14162  expmulz  14164  ccatopth2  14778  pfxccat3  14795  resqrtcl  15330  limsupgle  15554  o1add  15691  o1mul  15692  o1sub  15693  bitsfzo  16518  sadfval  16535  smufval  16560  nn0rppwr  16644  prmexpb  16803  4sqlem18  17047  vdwlem10  17075  fsets  17254  setsstruct2  17259  submre  17682  mrelatlub  18643  chnccat  18707  gsmsymgreqlem2  19532  mndodcong  19643  subgabl  19937  gex2abl  19952  ogrpinvlt  20245  rng1zrlem  20290  cntzsubrng  20703  cntzsubr  20742  abvres  20971  lbsind2  21239  lspsneu  21284  lbsextlem2  21320  lbsextg  21323  lindfind2  22005  matring  22637  maducoeval  22833  maducoeval2  22834  maduf  22835  madurid  22838  gsummatr01  22853  cramerimplem3  22879  cnprest  23483  hausnei2  23547  isreg2  23571  cmpcld  23596  llyrest  23679  nllyrest  23680  csdfil  24088  hausflimlem  24173  ssblps  24616  ssbl  24617  cphassi  25410  cphassir  25411  4cphipval2  25438  cphipval  25439  dvres2  26108  plyadd  26411  plymul  26412  coeeu  26419  vieta1  26510  aalioulem3  26534  aalioulem4  26535  efgh  26743  cxpadd  26881  cxpsub  26884  mulcxp  26887  divcxp  26889  cxple2  26899  cxplt2  26900  cxpcn3lem  26949  angcan  27004  ang180lem5  27015  isosctrlem3  27022  logexprlim  27426  lgssq  27538  abvcxp  27816  padicabv  27831  nosupbnd2lem1  27916  noinfbnd2lem1  27931  nosupinfsep  27933  noetalem1  27942  ltmuls2  28401  brbtwn2  29292  ax5seglem6  29321  axcontlem4  29354  axcontlem8  29358  uhgr2edg  29595  nbgrisvtx  29728  nbupgrres  29751  clwwlkccat  30378  clwwlknonex2lem2  30496  frgrreggt1  30781  chscllem4  32029  cshwrnid  33312  ifscgr  36557  matunitlindflem1  38308  lshpnelb  39799  lfl1  39885  lshpkrlem6  39930  lshpkrex  39933  hlrelat3  40227  atbtwnexOLDN  40262  atbtwnex  40263  3dim3  40284  3atlem5  40302  2llnmat  40339  lvolex3N  40353  lvolnle3at  40397  4atlem11  40424  4atlem12  40427  dalemccea  40498  cdlema2N  40607  paddasslem2  40636  atmod1i1m  40673  lhp2lt  40816  lhp0lt  40818  lhpj1  40837  lhpmcvr4N  40841  lhpelim  40852  lhpmod2i2  40853  lhpmod6i1  40854  cdlemb2  40856  lhple  40857  lhpat  40858  4atex  40891  4atex2-0aOLDN  40893  4atex3  40896  ldilco  40931  ltrncl  40940  ltrn11  40941  ltrnle  40944  ltrncnvleN  40945  ltrnm  40946  ltrnj  40947  ltrncvr  40948  ltrnatb  40952  ltrnel  40954  ltrncnvel  40957  ltrncnv  40961  trlval2  40978  trlcnv  40980  trljat1  40981  trljat2  40982  trl0  40985  ltrnnidn  40989  trlnidatb  40992  cdlemc1  41006  cdlemc2  41007  cdlemc5  41010  cdlemc6  41011  cdlemd3  41015  cdlemd6  41018  cdleme0aa  41025  cdleme0b  41027  cdleme0c  41028  cdleme0e  41032  cdleme0fN  41033  cdleme01N  41036  cdleme02N  41037  cdleme0ex1N  41038  cdleme0moN  41040  cdleme3g  41049  cdleme3h  41050  cdleme3  41052  cdleme4  41053  cdleme4a  41054  cdleme5  41055  cdleme8  41065  cdleme9  41068  cdleme10  41069  cdleme16aN  41074  cdleme11a  41075  cdleme11fN  41079  cdleme11g  41080  cdleme11h  41081  cdleme11j  41082  cdleme11k  41083  cdleme12  41086  cdleme13  41087  cdleme17c  41103  cdleme17d1  41104  cdleme18a  41106  cdleme18b  41107  cdleme18c  41108  cdleme22gb  41109  cdlemeda  41113  cdlemednpq  41114  cdlemednuN  41115  cdleme19c  41120  cdleme20aN  41124  cdleme20bN  41125  cdleme20c  41126  cdleme22aa  41154  cdleme22a  41155  cdleme22b  41156  cdleme22d  41158  cdleme22e  41159  cdleme27cl  41181  cdleme27a  41182  cdleme30a  41193  cdleme42a  41286  cdleme42c  41287  cdleme50laut  41362  cdlemf1  41376  cdlemf  41378  cdlemfnid  41379  trlord  41384  cdlemg2fv2  41415  cdlemg2kq  41417  cdlemg2m  41419  cdlemg4a  41423  cdlemg4d  41428  cdlemg4g  41431  cdlemg4  41432  cdlemg6c  41435  cdlemg7aN  41440  cdlemg8a  41442  cdlemg8b  41443  cdlemg8c  41444  cdlemg9a  41447  cdlemg9b  41448  cdlemg9  41449  cdlemg11aq  41453  cdlemg10c  41454  cdlemg12a  41458  cdlemg12b  41459  cdlemg12c  41460  cdlemg17a  41476  cdlemg18b  41494  cdlemg18c  41495  cdlemg31b0a  41510  cdlemg31a  41512  cdlemg31b  41513  cdlemg31d  41515  cdlemg35  41528  trlcoabs2N  41537  trlcolem  41541  cdlemg44a  41546  trljco  41555  trljco2  41556  tendoco2  41583  tendopltp  41595  cdlemi1  41633  cdlemi2  41634  cdlemj3  41638  tendocan  41639  cdlemk3  41648  cdlemk4  41649  cdlemk5a  41650  cdlemk9  41654  cdlemk9bN  41655  cdlemkvcl  41657  cdlemk10  41658  cdlemk30  41709  cdlemk31  41711  cdlemk39  41731  cdlemkfid1N  41736  cdlemkid1  41737  cdlemkid2  41739  cdlemkfid3N  41740  cdlemk19ylem  41745  cdlemk19xlem  41757  cdlemk19x  41758  cdlemk53b  41771  cdlemk53  41772  cdlemk54  41773  cdlemk55a  41774  cdlemk43N  41778  cdlemk19u1  41784  cdlemk19u  41785  cdleml1N  41791  erngdvlem4  41806  erngdvlem4-rN  41814  dia11N  41863  cdlemm10N  41933  dib11N  41975  cdlemn2  42010  cdlemn10  42021  dihjustlem  42031  dihord2cN  42036  dihlsscpre  42049  dih1dimb2  42056  dihvalcq2  42062  dihopelvalcpre  42063  dihord6b  42075  dih11  42080  dihmeetlem1N  42105  dihglblem2N  42109  dihglblem3N  42110  dihmeetlem2N  42114  dihglbcpreN  42115  dihmeetcN  42117  dihmeetbclemN  42119  dihmeetlem4preN  42121  dihmeetlem9N  42130  dihmeetlem20N  42141  dihlspsnssN  42147  dihlspsnat  42148  dihatlat  42149  dihglblem6  42155  dihmeet  42158  dochss  42180  hdmapval3N  42653  hgmap11  42717  remulcand  43241  congtr  43733  fzmaxdif  43749  isnumbasgrplem2  43872  ntrclsk13  44838  ssmapsn  45973  infleinf  46128  suplesup2  46132  supxrunb3  46155  mullimc  46373  mullimcf  46380  islpcn  46394  limsupresxr  46521  liminfresxr  46522  cncfuni  46641  icccncfext  46642  stoweidlem34  46789  stoweidlem59  46814  stirlinglem13  46841  fourierdlem41  46903  fourierdlem42  46904  fourierdlem73  46934  sge0iunmptlemfi  47168  meadjiunlem  47220  ovncvrrp  47319  sssmf  47493  smflimsuplem7  47581  smflimsuplem8  47582  ormkglobd  47632  funressneu  47825  grlimedgclnbgr  48801  lincscm  49251  lincext3  49277  el0ldep  49287  el0ldepsnzr  49288  itscnhlc0xyqsol  49586  uptr2  50040