Theorem simpll2 1101

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)

Assertion

Ref	Expression
simpll2	⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓)

Proof of Theorem simpll2

Step	Hyp	Ref	Expression
1		simpl2 1065	. 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜓)
2	1	adantr 481	1 ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  f1prex  6539  wemappo  8454  iunfictbso  8937  fin1a2lem13  9234  prlem934  9855  ifle  12028  ixxlb  12197  elfzonelfzo  12570  swrdcl  13419  subcn2  14325  qexpz  15605  mreexexd  16308  mreexexdOLD  16309  initoeu2lem2  16665  issubmnd  17318  gsumccat  17378  frmdup3lem  17403  pmtrf  17875  pgpssslw  18029  lsmmod  18088  reslmhm2b  19054  lsmcl  19083  lbsextlem3  19160  coe1mul2  19639  coe1fzgsumdlem  19671  evl1gsumdlem  19720  frlmsslsp  20135  islindf4  20177  scmate  20316  mdetdiaglem  20404  madurid  20450  cramerlem2  20494  pmatcollpw3lem  20588  iscnp4  21067  cnrest2  21090  ordthauslem  21187  cncmp  21195  clsconn  21233  rnelfmlem  21756  flimrest  21787  isfcf  21838  cnpfcf  21845  alexsubALT  21855  cldsubg  21914  utop2nei  22054  neipcfilu  22100  blssps  22229  blss  22230  stdbdbl  22322  metcnp3  22345  nmoeq0  22540  xrsxmet  22612  metdseq0  22657  addcnlem  22667  xrhmeo  22745  nmhmcn  22920  cfilres  23094  lgsfcl2  25028  lgsdir  25057  lgsne0  25060  istrkgcb  25355  axcontlem2  25845  axcontlem7  25850  axcontlem8  25851  subupgr  26179  wpthswwlks2on  26854  frgr3v  27139  numclwwlkovf2ex  27219  pjhthmo  28161  xrge0adddir  29692  pcmplfinf  29928  probun  30481  nosupbnd1lem3  31856  nosupbnd1lem4  31857  nosupbnd1lem5  31858  nosupbnd2  31862  trisegint  32135  btwnconn1lem13  32206  outsideoftr  32236  outsideofeq  32237  linethru  32260  isbasisrelowllem1  33203  atlatmstc  34606  cvlcvr1  34626  hlrelat  34688  intnatN  34693  cvrval5  34701  2at0mat0  34811  llncvrlpln  34844  lplnexllnN  34850  lplncvrlvol  34902  lncvrelatN  35067  lncmp  35069  paddasslem5  35110  pmapjoin  35138  pmapjat1  35139  pclclN  35177  lhprelat3N  35326  cdleme32fvcl  35728  cdlemg1a  35858  cdlemg1cN  35875  cdlemg39  36004  ltrncom  36026  dihmeetALTN  36616  dihlspsnat  36622  mapdrvallem2  36934  mzpsubst  37311  lzunuz  37331  acongeq  37550  jm2.19  37560  jm2.27  37575  aomclem6  37629  lmhmfgsplit  37656  hbtlem5  37698  iunrelexpuztr  38011  3adantll3  39203  ioondisj2  39714  ioondisj1  39715  iccintsng  39749  icccncfext  40100  stoweidlem61  40278  fourierdlem42  40366  fourierdlem73  40396  smflimlem2  40980  domnmsuppn0  42150  lincresunit3  42270  nnolog2flm1  42384