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  6292  f1prex  7225  poxp3  8090  fprlem2  8241  naddsuc2  8626  iunfictbso  10027  fin1a2lem13  10325  prlem934  10946  ifle  13117  ixxlb  13288  elfzonelfzo  13690  swrdcl  14570  subcn2  15520  qexpz  16831  mreexexd  17572  initoeu2lem2  17940  issubmnd  18653  frmdup3lem  18758  pmtrf  19352  pgpssslw  19511  lsmmod  19572  reslmhm2b  20976  lsmcl  21005  lbsextlem3  21085  frlmsslsp  21721  islindf4  21763  coe1mul2  22171  coe1fzgsumdlem  22206  evl1gsumdlem  22259  scmate  22413  mdetdiaglem  22501  madurid  22547  cramerlem2  22591  pmatcollpw3lem  22686  iscnp4  23166  cnrest2  23189  ordthauslem  23286  cncmp  23295  clsconn  23333  rnelfmlem  23855  flimrest  23886  isfcf  23937  cnpfcf  23944  alexsubALT  23954  cldsubg  24014  utop2nei  24154  neipcfilu  24199  blssps  24328  blss  24329  stdbdbl  24421  metcnp3  24444  nmoeq0  24640  xrsxmet  24714  metdseq0  24759  addcnlem  24769  xrhmeo  24860  nmhmcn  25036  cfilres  25212  lgsfcl2  27230  lgsdir  27259  lgsne0  27262  nosupbnd1lem3  27638  nosupbnd1lem4  27639  nosupbnd1lem5  27640  nosupbnd2  27644  noinfbnd1lem3  27653  noinfbnd1lem4  27654  noinfbnd1lem5  27655  noinfbnd2  27659  sltlpss  27840  sleadd1  27919  sltmul2  28097  istrkgcb  28419  axcontlem2  28928  axcontlem7  28933  axcontlem8  28934  subupgr  29250  clwwlknonex2  30071  frgr3v  30237  pjhthmo  31264  xrge0adddir  32985  dimvalfi  33573  pcmplfinf  33827  probun  34386  satfv1lem  35334  trisegint  36001  btwnconn1lem13  36072  outsideoftr  36102  outsideofeq  36103  linethru  36126  isbasisrelowllem1  37328  atlatmstc  39297  cvlcvr1  39317  hlrelat  39381  intnatN  39386  cvrval5  39394  2at0mat0  39504  llncvrlpln  39537  lplnexllnN  39543  lplncvrlvol  39595  lncvrelatN  39760  lncmp  39762  paddasslem5  39803  pmapjoin  39831  pmapjat1  39832  pclclN  39870  lhprelat3N  40019  cdleme32fvcl  40419  cdlemg1a  40549  cdlemg1cN  40566  cdlemg39  40695  ltrncom  40717  dihmeetALTN  41306  dihlspsnat  41312  mapdrvallem2  41624  sticksstones12  42131  mzpsubst  42721  lzunuz  42741  acongeq  42956  jm2.19  42966  jm2.27  42981  aomclem6  43032  lmhmfgsplit  43059  hbtlem5  43101  nadd2rabtr  43357  iunrelexpuztr  43692  ismnu  44234  3adantll3  45020  ioondisj2  45475  ioondisj1  45476  iccintsng  45505  icccncfext  45869  stoweidlem61  46043  fourierdlem42  46131  fourierdlem73  46161  smflimlem2  46754  domnmsuppn0  48354  lincresunit3  48467  nnolog2flm1  48576  itschlc0xyqsol1  48752  itschlc0xyqsol  48753