Theorem simpll2 1211

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)

Assertion

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

Proof of Theorem simpll2

Step	Hyp	Ref	Expression
1		simp2 1135	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜓)
2	1	ad2antrr 722	1 ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  frpomin  6228  f1prex  7136  fprlem2  8088  iunfictbso  9801  fin1a2lem13  10099  prlem934  10720  ifle  12860  ixxlb  13030  elfzonelfzo  13417  swrdcl  14286  subcn2  15232  qexpz  16530  mreexexd  17274  initoeu2lem2  17646  issubmnd  18327  gsumccatOLD  18394  frmdup3lem  18420  pmtrf  18978  pgpssslw  19134  lsmmod  19196  reslmhm2b  20231  lsmcl  20260  lbsextlem3  20337  frlmsslsp  20913  islindf4  20955  coe1mul2  21350  coe1fzgsumdlem  21382  evl1gsumdlem  21432  scmate  21567  mdetdiaglem  21655  madurid  21701  cramerlem2  21745  pmatcollpw3lem  21840  iscnp4  22322  cnrest2  22345  ordthauslem  22442  cncmp  22451  clsconn  22489  rnelfmlem  23011  flimrest  23042  isfcf  23093  cnpfcf  23100  alexsubALT  23110  cldsubg  23170  utop2nei  23310  neipcfilu  23356  blssps  23485  blss  23486  stdbdbl  23579  metcnp3  23602  nmoeq0  23806  xrsxmet  23878  metdseq0  23923  addcnlem  23933  xrhmeo  24015  nmhmcn  24189  cfilres  24365  lgsfcl2  26356  lgsdir  26385  lgsne0  26388  istrkgcb  26721  axcontlem2  27236  axcontlem7  27241  axcontlem8  27242  subupgr  27557  clwwlknonex2  28374  frgr3v  28540  pjhthmo  29565  xrge0adddir  31203  dimvalfi  31589  pcmplfinf  31713  probun  32286  satfv1lem  33224  nosupbnd1lem3  33840  nosupbnd1lem4  33841  nosupbnd1lem5  33842  nosupbnd2  33846  noinfbnd1lem3  33855  noinfbnd1lem4  33856  noinfbnd1lem5  33857  noinfbnd2  33861  sltlpss  34014  trisegint  34257  btwnconn1lem13  34328  outsideoftr  34358  outsideofeq  34359  linethru  34382  isbasisrelowllem1  35453  atlatmstc  37260  cvlcvr1  37280  hlrelat  37343  intnatN  37348  cvrval5  37356  2at0mat0  37466  llncvrlpln  37499  lplnexllnN  37505  lplncvrlvol  37557  lncvrelatN  37722  lncmp  37724  paddasslem5  37765  pmapjoin  37793  pmapjat1  37794  pclclN  37832  lhprelat3N  37981  cdleme32fvcl  38381  cdlemg1a  38511  cdlemg1cN  38528  cdlemg39  38657  ltrncom  38679  dihmeetALTN  39268  dihlspsnat  39274  mapdrvallem2  39586  sticksstones12  40042  mzpsubst  40486  lzunuz  40506  acongeq  40721  jm2.19  40731  jm2.27  40746  aomclem6  40800  lmhmfgsplit  40827  hbtlem5  40869  iunrelexpuztr  41216  ismnu  41768  3adantll3  42476  ioondisj2  42921  ioondisj1  42922  iccintsng  42951  icccncfext  43318  stoweidlem61  43492  fourierdlem42  43580  fourierdlem73  43610  smflimlem2  44194  domnmsuppn0  45593  lincresunit3  45710  nnolog2flm1  45824  itschlc0xyqsol1  46000  itschlc0xyqsol  46001