Theorem simpll2 1230

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  frpomin  6331  f1prex  7272  poxp3  8134  fprlem2  8286  naddsuc2  8676  iunfictbso  10086  fin1a2lem13  10384  prlem934  11006  ifle  13214  ixxlb  13385  elfzonelfzo  13789  swrdcl  14673  subcn2  15636  qexpz  16951  mreexexd  17694  initoeu2lem2  18062  issubmnd  18809  frmdup3lem  18915  pmtrf  19516  pgpssslw  19675  lsmmod  19736  reslmhm2b  21144  lsmcl  21173  lbsextlem3  21253  frlmsslsp  21906  islindf4  21948  coe1mul2  22390  coe1fzgsumdlem  22424  evl1gsumdlem  22477  scmate  22628  mdetdiaglem  22716  madurid  22762  cramerlem2  22806  pmatcollpw3lem  22901  iscnp4  23381  cnrest2  23404  ordthauslem  23501  cncmp  23510  clsconn  23548  rnelfmlem  24070  flimrest  24101  isfcf  24152  cnpfcf  24159  alexsubALT  24169  cldsubg  24229  utop2nei  24368  neipcfilu  24413  blssps  24542  blss  24543  stdbdbl  24635  metcnp3  24658  nmoeq0  24854  xrsxmet  24928  metdseq0  24973  addcnlem  24983  xrhmeo  25066  nmhmcn  25240  cfilres  25416  lgsfcl2  27425  lgsdir  27454  lgsne0  27457  nosupbnd1lem3  27832  nosupbnd1lem4  27833  nosupbnd1lem5  27834  nosupbnd2  27838  noinfbnd1lem3  27847  noinfbnd1lem4  27848  noinfbnd1lem5  27849  noinfbnd2  27853  ltslpss  28059  leadds1  28140  ltmuls2  28322  bdayfinbndlem1  28618  istrkgcb  28683  axcontlem2  29224  axcontlem7  29229  axcontlem8  29230  subupgr  29546  clwwlknonex2  30369  frgr3v  30535  pjhthmo  31563  xrge0adddir  33251  dimvalfi  33909  pcmplfinf  34168  probun  34726  satfv1lem  35725  trisegint  36391  btwnconn1lem13  36462  outsideoftr  36492  outsideofeq  36493  linethru  36516  isbasisrelowllem1  37861  atlatmstc  39955  cvlcvr1  39975  hlrelat  40038  intnatN  40043  cvrval5  40051  2at0mat0  40161  llncvrlpln  40194  lplnexllnN  40200  lplncvrlvol  40252  lncvrelatN  40417  lncmp  40419  paddasslem5  40460  pmapjoin  40488  pmapjat1  40489  pclclN  40527  lhprelat3N  40676  cdleme32fvcl  41076  cdlemg1a  41206  cdlemg1cN  41223  cdlemg39  41352  ltrncom  41374  dihmeetALTN  41963  dihlspsnat  41969  mapdrvallem2  42281  sticksstones12  42787  mzpsubst  43341  lzunuz  43361  acongeq  43572  jm2.19  43582  jm2.27  43597  aomclem6  43648  lmhmfgsplit  43675  hbtlem5  43717  nadd2rabtr  43973  iunrelexpuztr  44307  ismnu  44835  3adantll3  45620  ioondisj2  46067  ioondisj1  46068  iccintsng  46097  icccncfext  46459  stoweidlem61  46633  fourierdlem42  46721  fourierdlem73  46751  smflimlem2  47344  domnmsuppn0  49000  lincresunit3  49112  nnolog2flm1  49221  itschlc0xyqsol1  49397  itschlc0xyqsol  49398