Theorem simpll2 1209

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  f1prex  7040  wemappo  9013  iunfictbso  9540  fin1a2lem13  9834  prlem934  10455  ifle  12591  ixxlb  12761  elfzonelfzo  13140  swrdcl  14007  subcn2  14951  qexpz  16237  mreexexd  16919  initoeu2lem2  17275  issubmnd  17938  gsumccatOLD  18005  frmdup3lem  18031  pmtrf  18583  pgpssslw  18739  lsmmod  18801  reslmhm2b  19826  lsmcl  19855  lbsextlem3  19932  coe1mul2  20437  coe1fzgsumdlem  20469  evl1gsumdlem  20519  frlmsslsp  20940  islindf4  20982  scmate  21119  mdetdiaglem  21207  madurid  21253  cramerlem2  21297  pmatcollpw3lem  21391  iscnp4  21871  cnrest2  21894  ordthauslem  21991  cncmp  22000  clsconn  22038  rnelfmlem  22560  flimrest  22591  isfcf  22642  cnpfcf  22649  alexsubALT  22659  cldsubg  22719  utop2nei  22859  neipcfilu  22905  blssps  23034  blss  23035  stdbdbl  23127  metcnp3  23150  nmoeq0  23345  xrsxmet  23417  metdseq0  23462  addcnlem  23472  xrhmeo  23550  nmhmcn  23724  cfilres  23899  lgsfcl2  25879  lgsdir  25908  lgsne0  25911  istrkgcb  26242  axcontlem2  26751  axcontlem7  26756  axcontlem8  26757  subupgr  27069  clwwlknonex2  27888  frgr3v  28054  pjhthmo  29079  xrge0adddir  30679  dimvalfi  31002  pcmplfinf  31125  probun  31677  satfv1lem  32609  frpomin  33078  fprlem2  33138  nosupbnd1lem3  33210  nosupbnd1lem4  33211  nosupbnd1lem5  33212  nosupbnd2  33216  trisegint  33489  btwnconn1lem13  33560  outsideoftr  33590  outsideofeq  33591  linethru  33614  isbasisrelowllem1  34639  atlatmstc  36470  cvlcvr1  36490  hlrelat  36553  intnatN  36558  cvrval5  36566  2at0mat0  36676  llncvrlpln  36709  lplnexllnN  36715  lplncvrlvol  36767  lncvrelatN  36932  lncmp  36934  paddasslem5  36975  pmapjoin  37003  pmapjat1  37004  pclclN  37042  lhprelat3N  37191  cdleme32fvcl  37591  cdlemg1a  37721  cdlemg1cN  37738  cdlemg39  37867  ltrncom  37889  dihmeetALTN  38478  dihlspsnat  38484  mapdrvallem2  38796  mzpsubst  39394  lzunuz  39414  acongeq  39629  jm2.19  39639  jm2.27  39654  aomclem6  39708  lmhmfgsplit  39735  hbtlem5  39777  iunrelexpuztr  40113  ismnu  40646  3adantll3  41350  ioondisj2  41816  ioondisj1  41817  iccintsng  41848  icccncfext  42219  stoweidlem61  42395  fourierdlem42  42483  fourierdlem73  42513  smflimlem2  43097  domnmsuppn0  44466  lincresunit3  44585  nnolog2flm1  44699  itschlc0xyqsol1  44802  itschlc0xyqsol  44803