Theorem simpll2 1232

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

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

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 1105

This theorem is referenced by:  frpomin  6343  f1prex  7284  poxp3  8147  fprlem2  8299  naddsuc2  8689  iunfictbso  10099  fin1a2lem13  10397  prlem934  11019  ifle  13224  ixxlb  13395  elfzonelfzo  13800  swrdcl  14685  subcn2  15648  qexpz  16962  mreexexd  17705  initoeu2lem2  18073  issubmnd  18820  frmdup3lem  18926  pmtrf  19526  pgpssslw  19685  lsmmod  19746  reslmhm2b  21156  lsmcl  21185  lbsextlem3  21265  frlmsslsp  21927  islindf4  21969  coe1mul2  22411  coe1fzgsumdlem  22444  evl1gsumdlem  22497  scmate  22648  mdetdiaglem  22736  madurid  22782  cramerlem2  22826  pmatcollpw3lem  22921  iscnp4  23401  cnrest2  23424  ordthauslem  23521  cncmp  23530  clsconn  23568  rnelfmlem  24090  flimrest  24121  isfcf  24172  cnpfcf  24179  alexsubALT  24189  cldsubg  24249  utop2nei  24388  neipcfilu  24433  blssps  24562  blss  24563  stdbdbl  24655  metcnp3  24678  nmoeq0  24874  xrsxmet  24948  metdseq0  24993  addcnlem  25003  xrhmeo  25086  nmhmcn  25260  cfilres  25436  lgsfcl2  27445  lgsdir  27474  lgsne0  27477  nosupbnd1lem3  27852  nosupbnd1lem4  27853  nosupbnd1lem5  27854  nosupbnd2  27858  noinfbnd1lem3  27867  noinfbnd1lem4  27868  noinfbnd1lem5  27869  noinfbnd2  27873  ltslpss  28079  leadds1  28160  ltmuls2  28342  bdayfinbndlem1  28638  istrkgcb  28703  axcontlem2  29293  axcontlem7  29298  axcontlem8  29299  subupgr  29615  clwwlknonex2  30438  frgr3v  30604  pjhthmo  31632  xrge0adddir  33316  dimvalfi  33970  pcmplfinf  34229  probun  34787  satfv1lem  35832  trisegint  36498  btwnconn1lem13  36569  outsideoftr  36599  outsideofeq  36600  linethru  36623  isbasisrelowllem1  37979  atlatmstc  40071  cvlcvr1  40091  hlrelat  40154  intnatN  40159  cvrval5  40167  2at0mat0  40277  llncvrlpln  40310  lplnexllnN  40316  lplncvrlvol  40368  lncvrelatN  40533  lncmp  40535  paddasslem5  40576  pmapjoin  40604  pmapjat1  40605  pclclN  40643  lhprelat3N  40792  cdleme32fvcl  41192  cdlemg1a  41322  cdlemg1cN  41339  cdlemg39  41468  ltrncom  41490  dihmeetALTN  42079  dihlspsnat  42085  mapdrvallem2  42397  sticksstones12  42903  mzpsubst  43459  lzunuz  43479  acongeq  43690  jm2.19  43700  jm2.27  43715  aomclem6  43766  lmhmfgsplit  43793  hbtlem5  43835  nadd2rabtr  44091  iunrelexpuztr  44425  ismnu  44951  3adantll3  45742  ioondisj2  46189  ioondisj1  46190  iccintsng  46219  icccncfext  46581  stoweidlem61  46755  fourierdlem42  46843  fourierdlem73  46873  smflimlem2  47466  domnmsuppn0  49126  lincresunit3  49238  nnolog2flm1  49347  itschlc0xyqsol1  49523  itschlc0xyqsol  49524