Theorem simpll2 1094

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

Assertion

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

Proof of Theorem simpll2

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

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  f1prex  6439  wemappo  8337  iunfictbso  8820  fin1a2lem13  9117  prlem934  9734  ifle  11902  ixxlb  12068  elfzonelfzo  12436  swrdcl  13271  subcn2  14173  qexpz  15443  mreexexd  16131  mreexexdOLD  16132  initoeu2lem2  16488  issubmnd  17141  gsumccat  17201  frmdup3lem  17226  pmtrf  17698  pgpssslw  17852  lsmmod  17911  reslmhm2b  18875  lsmcl  18904  lbsextlem3  18981  coe1mul2  19460  coe1fzgsumdlem  19492  evl1gsumdlem  19541  frlmsslsp  19954  islindf4  19996  scmate  20135  mdetdiaglem  20223  madurid  20269  cramerlem2  20313  pmatcollpw3lem  20407  iscnp4  20877  cnrest2  20900  ordthauslem  20997  cncmp  21005  clscon  21043  rnelfmlem  21566  flimrest  21597  isfcf  21648  cnpfcf  21655  alexsubALT  21665  cldsubg  21724  utop2nei  21864  neipcfilu  21910  blssps  22039  blss  22040  stdbdbl  22132  metcnp3  22155  nmoeq0  22350  xrsxmet  22420  metdseq0  22465  addcnlem  22475  xrhmeo  22553  nmhmcn  22728  cfilres  22902  lgsfcl2  24828  lgsdir  24857  lgsne0  24860  istrkgcb  25155  axcontlem2  25645  axcontlem7  25650  axcontlem8  25651  usg2spot2nb  26592  pjhthmo  27545  xrge0adddir  29023  pcmplfinf  29256  probun  29808  trisegint  31305  btwnconn1lem13  31376  outsideoftr  31406  outsideofeq  31407  linethru  31430  isbasisrelowllem1  32379  atlatmstc  33624  cvlcvr1  33644  hlrelat  33706  intnatN  33711  cvrval5  33719  2at0mat0  33829  llncvrlpln  33862  lplnexllnN  33868  lplncvrlvol  33920  lncvrelatN  34085  lncmp  34087  paddasslem5  34128  pmapjoin  34156  pmapjat1  34157  pclclN  34195  lhprelat3N  34344  cdleme32fvcl  34746  cdlemg1a  34876  cdlemg1cN  34893  cdlemg39  35022  ltrncom  35044  dihmeetALTN  35634  dihlspsnat  35640  mapdrvallem2  35952  mzpsubst  36329  lzunuz  36349  acongeq  36568  jm2.19  36578  jm2.27  36593  aomclem6  36647  lmhmfgsplit  36674  hbtlem5  36717  iunrelexpuztr  37030  3adantll3  38226  ioondisj2  38561  ioondisj1  38562  iccintsng  38596  icccncfext  38773  stoweidlem61  38954  fourierdlem42  39042  fourierdlem73  39072  smflimlem2  39658  subupgr  40511  wpthswwlks2on  41164  frgr3v  41445  domnmsuppn0  41944  lincresunit3  42064  nnolog2flm1  42182