Theorem simpll2 1213

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 724	1 ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓)

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

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

This theorem is referenced by:  frpomin  6341  f1prex  7281  poxp3  8135  fprlem2  8285  iunfictbso  10108  fin1a2lem13  10406  prlem934  11027  ifle  13175  ixxlb  13345  elfzonelfzo  13733  swrdcl  14594  subcn2  15538  qexpz  16833  mreexexd  17591  initoeu2lem2  17964  issubmnd  18651  frmdup3lem  18746  pmtrf  19322  pgpssslw  19481  lsmmod  19542  reslmhm2b  20664  lsmcl  20693  lbsextlem3  20772  frlmsslsp  21350  islindf4  21392  coe1mul2  21790  coe1fzgsumdlem  21824  evl1gsumdlem  21874  scmate  22011  mdetdiaglem  22099  madurid  22145  cramerlem2  22189  pmatcollpw3lem  22284  iscnp4  22766  cnrest2  22789  ordthauslem  22886  cncmp  22895  clsconn  22933  rnelfmlem  23455  flimrest  23486  isfcf  23537  cnpfcf  23544  alexsubALT  23554  cldsubg  23614  utop2nei  23754  neipcfilu  23800  blssps  23929  blss  23930  stdbdbl  24025  metcnp3  24048  nmoeq0  24252  xrsxmet  24324  metdseq0  24369  addcnlem  24379  xrhmeo  24461  nmhmcn  24635  cfilres  24812  lgsfcl2  26803  lgsdir  26832  lgsne0  26835  nosupbnd1lem3  27210  nosupbnd1lem4  27211  nosupbnd1lem5  27212  nosupbnd2  27216  noinfbnd1lem3  27225  noinfbnd1lem4  27226  noinfbnd1lem5  27227  noinfbnd2  27231  sltlpss  27398  sleadd1  27469  sltmul2  27620  istrkgcb  27704  axcontlem2  28220  axcontlem7  28225  axcontlem8  28226  subupgr  28541  clwwlknonex2  29359  frgr3v  29525  pjhthmo  30550  xrge0adddir  32188  dimvalfi  32682  pcmplfinf  32836  probun  33413  satfv1lem  34348  trisegint  34995  btwnconn1lem13  35066  outsideoftr  35096  outsideofeq  35097  linethru  35120  isbasisrelowllem1  36231  atlatmstc  38184  cvlcvr1  38204  hlrelat  38268  intnatN  38273  cvrval5  38281  2at0mat0  38391  llncvrlpln  38424  lplnexllnN  38430  lplncvrlvol  38482  lncvrelatN  38647  lncmp  38649  paddasslem5  38690  pmapjoin  38718  pmapjat1  38719  pclclN  38757  lhprelat3N  38906  cdleme32fvcl  39306  cdlemg1a  39436  cdlemg1cN  39453  cdlemg39  39582  ltrncom  39604  dihmeetALTN  40193  dihlspsnat  40199  mapdrvallem2  40511  sticksstones12  40969  mzpsubst  41476  lzunuz  41496  acongeq  41712  jm2.19  41722  jm2.27  41737  aomclem6  41791  lmhmfgsplit  41818  hbtlem5  41860  nadd2rabtr  42124  naddsuc2  42133  iunrelexpuztr  42460  ismnu  43010  3adantll3  43716  ioondisj2  44196  ioondisj1  44197  iccintsng  44226  icccncfext  44593  stoweidlem61  44767  fourierdlem42  44855  fourierdlem73  44885  smflimlem2  45478  domnmsuppn0  47035  lincresunit3  47152  nnolog2flm1  47266  itschlc0xyqsol1  47442  itschlc0xyqsol  47443