Theorem simpll2 1214

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 1137	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜓)
2	1	ad2antrr 726	1 ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓)

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

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  frpomin  6287  f1prex  7218  poxp3  8080  fprlem2  8231  naddsuc2  8616  iunfictbso  10002  fin1a2lem13  10300  prlem934  10921  ifle  13093  ixxlb  13264  elfzonelfzo  13666  swrdcl  14550  subcn2  15499  qexpz  16810  mreexexd  17551  initoeu2lem2  17919  issubmnd  18666  frmdup3lem  18771  pmtrf  19365  pgpssslw  19524  lsmmod  19585  reslmhm2b  20986  lsmcl  21015  lbsextlem3  21095  frlmsslsp  21731  islindf4  21773  coe1mul2  22181  coe1fzgsumdlem  22216  evl1gsumdlem  22269  scmate  22423  mdetdiaglem  22511  madurid  22557  cramerlem2  22601  pmatcollpw3lem  22696  iscnp4  23176  cnrest2  23199  ordthauslem  23296  cncmp  23305  clsconn  23343  rnelfmlem  23865  flimrest  23896  isfcf  23947  cnpfcf  23954  alexsubALT  23964  cldsubg  24024  utop2nei  24163  neipcfilu  24208  blssps  24337  blss  24338  stdbdbl  24430  metcnp3  24453  nmoeq0  24649  xrsxmet  24723  metdseq0  24768  addcnlem  24778  xrhmeo  24869  nmhmcn  25045  cfilres  25221  lgsfcl2  27239  lgsdir  27268  lgsne0  27271  nosupbnd1lem3  27647  nosupbnd1lem4  27648  nosupbnd1lem5  27649  nosupbnd2  27653  noinfbnd1lem3  27662  noinfbnd1lem4  27663  noinfbnd1lem5  27664  noinfbnd2  27668  sltlpss  27851  sleadd1  27930  sltmul2  28108  istrkgcb  28432  axcontlem2  28941  axcontlem7  28946  axcontlem8  28947  subupgr  29263  clwwlknonex2  30084  frgr3v  30250  pjhthmo  31277  xrge0adddir  32994  dimvalfi  33609  pcmplfinf  33869  probun  34427  satfv1lem  35394  trisegint  36061  btwnconn1lem13  36132  outsideoftr  36162  outsideofeq  36163  linethru  36186  isbasisrelowllem1  37388  atlatmstc  39357  cvlcvr1  39377  hlrelat  39440  intnatN  39445  cvrval5  39453  2at0mat0  39563  llncvrlpln  39596  lplnexllnN  39602  lplncvrlvol  39654  lncvrelatN  39819  lncmp  39821  paddasslem5  39862  pmapjoin  39890  pmapjat1  39891  pclclN  39929  lhprelat3N  40078  cdleme32fvcl  40478  cdlemg1a  40608  cdlemg1cN  40625  cdlemg39  40754  ltrncom  40776  dihmeetALTN  41365  dihlspsnat  41371  mapdrvallem2  41683  sticksstones12  42190  mzpsubst  42780  lzunuz  42800  acongeq  43015  jm2.19  43025  jm2.27  43040  aomclem6  43091  lmhmfgsplit  43118  hbtlem5  43160  nadd2rabtr  43416  iunrelexpuztr  43751  ismnu  44293  3adantll3  45078  ioondisj2  45532  ioondisj1  45533  iccintsng  45562  icccncfext  45924  stoweidlem61  46098  fourierdlem42  46186  fourierdlem73  46216  smflimlem2  46809  domnmsuppn0  48399  lincresunit3  48512  nnolog2flm1  48621  itschlc0xyqsol1  48797  itschlc0xyqsol  48798