Theorem simp1l 1204

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  simp11l  1291  simp21l  1297  simp31l  1303  2f1fvneq  7211  eqfunresadj  7311  tfisi  7806  offsplitfpar  8065  poseq  8105  omeulem2  8515  uniinqs  8741  unxpdomlem3  9165  elfiun  9340  cantnffval  9582  tcrank  9806  cofsmo  10189  isfin2-2  10239  tskint  10706  tskun  10707  tskurn  10710  gruina  10739  dedekind  11307  subaddmulsub  11611  dmdcan  11863  lt2msq1  12038  supmullem1  12124  supmul  12126  xaddass  13199  xaddass2  13200  xlt2add  13210  xmulasslem3  13236  xadddi2r  13248  iccsplit  13436  expaddzlem  14065  expaddz  14066  expmulz  14068  ccatopth2  14677  pfxccat3  14694  resqrtcl  15213  limsupgle  15437  o1add  15574  o1mul  15575  o1sub  15576  bitsfzo  16402  sadfval  16419  smufval  16444  nn0rppwr  16528  prmexpb  16687  4sqlem18  16931  vdwlem10  16959  fsets  17137  setsstruct2  17142  submre  17565  mrelatlub  18526  chnccat  18590  gsmsymgreqlem2  19404  mndodcong  19515  subgabl  19809  gex2abl  19824  ogrpinvlt  20117  cntzsubrng  20546  cntzsubr  20585  abvres  20810  lbsind2  21078  lspsneu  21123  lbsextlem2  21159  lbsextg  21162  lindfind2  21800  matring  22433  maducoeval  22629  maducoeval2  22630  maduf  22631  madurid  22634  gsummatr01  22649  cramerimplem3  22675  cnprest  23279  hausnei2  23343  isreg2  23367  cmpcld  23392  llyrest  23475  nllyrest  23476  csdfil  23884  hausflimlem  23969  ssblps  24412  ssbl  24413  cphassi  25206  cphassir  25207  4cphipval2  25234  cphipval  25235  dvres2  25904  plyadd  26207  plymul  26208  coeeu  26215  vieta1  26303  aalioulem3  26325  aalioulem4  26326  efgh  26530  cxpadd  26668  cxpsub  26671  mulcxp  26674  divcxp  26676  cxple2  26686  cxplt2  26687  cxpcn3lem  26736  angcan  26791  ang180lem5  26802  isosctrlem3  26809  logexprlim  27213  lgssq  27325  abvcxp  27603  padicabv  27618  nosupbnd2lem1  27704  noinfbnd2lem1  27719  nosupinfsep  27721  noetalem1  27730  ltmuls2  28188  brbtwn2  28999  ax5seglem6  29028  axcontlem4  29061  axcontlem8  29065  uhgr2edg  29302  nbgrisvtx  29435  nbupgrres  29458  clwwlkccat  30085  clwwlknonex2lem2  30203  frgrreggt1  30488  chscllem4  31736  cshwrnid  33047  ifscgr  36279  matunitlindflem1  37990  lshpnelb  39483  lfl1  39569  lshpkrlem6  39614  lshpkrex  39617  hlrelat3  39911  atbtwnexOLDN  39946  atbtwnex  39947  3dim3  39968  3atlem5  39986  2llnmat  40023  lvolex3N  40037  lvolnle3at  40081  4atlem11  40108  4atlem12  40111  dalemccea  40182  cdlema2N  40291  paddasslem2  40320  atmod1i1m  40357  lhp2lt  40500  lhp0lt  40502  lhpj1  40521  lhpmcvr4N  40525  lhpelim  40536  lhpmod2i2  40537  lhpmod6i1  40538  cdlemb2  40540  lhple  40541  lhpat  40542  4atex  40575  4atex2-0aOLDN  40577  4atex3  40580  ldilco  40615  ltrncl  40624  ltrn11  40625  ltrnle  40628  ltrncnvleN  40629  ltrnm  40630  ltrnj  40631  ltrncvr  40632  ltrnatb  40636  ltrnel  40638  ltrncnvel  40641  ltrncnv  40645  trlval2  40662  trlcnv  40664  trljat1  40665  trljat2  40666  trl0  40669  ltrnnidn  40673  trlnidatb  40676  cdlemc1  40690  cdlemc2  40691  cdlemc5  40694  cdlemc6  40695  cdlemd3  40699  cdlemd6  40702  cdleme0aa  40709  cdleme0b  40711  cdleme0c  40712  cdleme0e  40716  cdleme0fN  40717  cdleme01N  40720  cdleme02N  40721  cdleme0ex1N  40722  cdleme0moN  40724  cdleme3g  40733  cdleme3h  40734  cdleme3  40736  cdleme4  40737  cdleme4a  40738  cdleme5  40739  cdleme8  40749  cdleme9  40752  cdleme10  40753  cdleme16aN  40758  cdleme11a  40759  cdleme11fN  40763  cdleme11g  40764  cdleme11h  40765  cdleme11j  40766  cdleme11k  40767  cdleme12  40770  cdleme13  40771  cdleme17c  40787  cdleme17d1  40788  cdleme18a  40790  cdleme18b  40791  cdleme18c  40792  cdleme22gb  40793  cdlemeda  40797  cdlemednpq  40798  cdlemednuN  40799  cdleme19c  40804  cdleme20aN  40808  cdleme20bN  40809  cdleme20c  40810  cdleme22aa  40838  cdleme22a  40839  cdleme22b  40840  cdleme22d  40842  cdleme22e  40843  cdleme27cl  40865  cdleme27a  40866  cdleme30a  40877  cdleme42a  40970  cdleme42c  40971  cdleme50laut  41046  cdlemf1  41060  cdlemf  41062  cdlemfnid  41063  trlord  41068  cdlemg2fv2  41099  cdlemg2kq  41101  cdlemg2m  41103  cdlemg4a  41107  cdlemg4d  41112  cdlemg4g  41115  cdlemg4  41116  cdlemg6c  41119  cdlemg7aN  41124  cdlemg8a  41126  cdlemg8b  41127  cdlemg8c  41128  cdlemg9a  41131  cdlemg9b  41132  cdlemg9  41133  cdlemg11aq  41137  cdlemg10c  41138  cdlemg12a  41142  cdlemg12b  41143  cdlemg12c  41144  cdlemg17a  41160  cdlemg18b  41178  cdlemg18c  41179  cdlemg31b0a  41194  cdlemg31a  41196  cdlemg31b  41197  cdlemg31d  41199  cdlemg35  41212  trlcoabs2N  41221  trlcolem  41225  cdlemg44a  41230  trljco  41239  trljco2  41240  tendoco2  41267  tendopltp  41279  cdlemi1  41317  cdlemi2  41318  cdlemj3  41322  tendocan  41323  cdlemk3  41332  cdlemk4  41333  cdlemk5a  41334  cdlemk9  41338  cdlemk9bN  41339  cdlemkvcl  41341  cdlemk10  41342  cdlemk30  41393  cdlemk31  41395  cdlemk39  41415  cdlemkfid1N  41420  cdlemkid1  41421  cdlemkid2  41423  cdlemkfid3N  41424  cdlemk19ylem  41429  cdlemk19xlem  41441  cdlemk19x  41442  cdlemk53b  41455  cdlemk53  41456  cdlemk54  41457  cdlemk55a  41458  cdlemk43N  41462  cdlemk19u1  41468  cdlemk19u  41469  cdleml1N  41475  erngdvlem4  41490  erngdvlem4-rN  41498  dia11N  41547  cdlemm10N  41617  dib11N  41659  cdlemn2  41694  cdlemn10  41705  dihjustlem  41715  dihord2cN  41720  dihlsscpre  41733  dih1dimb2  41740  dihvalcq2  41746  dihopelvalcpre  41747  dihord6b  41759  dih11  41764  dihmeetlem1N  41789  dihglblem2N  41793  dihglblem3N  41794  dihmeetlem2N  41798  dihglbcpreN  41799  dihmeetcN  41801  dihmeetbclemN  41803  dihmeetlem4preN  41805  dihmeetlem9N  41814  dihmeetlem20N  41825  dihlspsnssN  41831  dihlspsnat  41832  dihatlat  41833  dihglblem6  41839  dihmeet  41842  dochss  41864  hdmapval3N  42337  hgmap11  42401  remulcand  42923  congtr  43417  fzmaxdif  43433  isnumbasgrplem2  43556  ntrclsk13  44522  ssmapsn  45668  infleinf  45823  suplesup2  45827  supxrunb3  45850  mullimc  46068  mullimcf  46075  islpcn  46089  limsupresxr  46216  liminfresxr  46217  cncfuni  46336  icccncfext  46337  stoweidlem34  46484  stoweidlem59  46509  stirlinglem13  46536  fourierdlem41  46598  fourierdlem42  46599  fourierdlem73  46629  sge0iunmptlemfi  46863  meadjiunlem  46915  ovncvrrp  47014  sssmf  47188  smflimsuplem7  47276  smflimsuplem8  47277  ormkglobd  47327  funressneu  47517  grlimedgclnbgr  48493  lincscm  48928  lincext3  48954  el0ldep  48964  el0ldepsnzr  48965  itscnhlc0xyqsol  49263  uptr2  49718