Theorem simpll2 1212

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  frpomin  6243  f1prex  7156  fprlem2  8117  iunfictbso  9870  fin1a2lem13  10168  prlem934  10789  ifle  12931  ixxlb  13101  elfzonelfzo  13489  swrdcl  14358  subcn2  15304  qexpz  16602  mreexexd  17357  initoeu2lem2  17730  issubmnd  18412  gsumccatOLD  18479  frmdup3lem  18505  pmtrf  19063  pgpssslw  19219  lsmmod  19281  reslmhm2b  20316  lsmcl  20345  lbsextlem3  20422  frlmsslsp  21003  islindf4  21045  coe1mul2  21440  coe1fzgsumdlem  21472  evl1gsumdlem  21522  scmate  21659  mdetdiaglem  21747  madurid  21793  cramerlem2  21837  pmatcollpw3lem  21932  iscnp4  22414  cnrest2  22437  ordthauslem  22534  cncmp  22543  clsconn  22581  rnelfmlem  23103  flimrest  23134  isfcf  23185  cnpfcf  23192  alexsubALT  23202  cldsubg  23262  utop2nei  23402  neipcfilu  23448  blssps  23577  blss  23578  stdbdbl  23673  metcnp3  23696  nmoeq0  23900  xrsxmet  23972  metdseq0  24017  addcnlem  24027  xrhmeo  24109  nmhmcn  24283  cfilres  24460  lgsfcl2  26451  lgsdir  26480  lgsne0  26483  istrkgcb  26817  axcontlem2  27333  axcontlem7  27338  axcontlem8  27339  subupgr  27654  clwwlknonex2  28473  frgr3v  28639  pjhthmo  29664  xrge0adddir  31301  dimvalfi  31687  pcmplfinf  31811  probun  32386  satfv1lem  33324  nosupbnd1lem3  33913  nosupbnd1lem4  33914  nosupbnd1lem5  33915  nosupbnd2  33919  noinfbnd1lem3  33928  noinfbnd1lem4  33929  noinfbnd1lem5  33930  noinfbnd2  33934  sltlpss  34087  trisegint  34330  btwnconn1lem13  34401  outsideoftr  34431  outsideofeq  34432  linethru  34455  isbasisrelowllem1  35526  atlatmstc  37333  cvlcvr1  37353  hlrelat  37416  intnatN  37421  cvrval5  37429  2at0mat0  37539  llncvrlpln  37572  lplnexllnN  37578  lplncvrlvol  37630  lncvrelatN  37795  lncmp  37797  paddasslem5  37838  pmapjoin  37866  pmapjat1  37867  pclclN  37905  lhprelat3N  38054  cdleme32fvcl  38454  cdlemg1a  38584  cdlemg1cN  38601  cdlemg39  38730  ltrncom  38752  dihmeetALTN  39341  dihlspsnat  39347  mapdrvallem2  39659  sticksstones12  40114  mzpsubst  40570  lzunuz  40590  acongeq  40805  jm2.19  40815  jm2.27  40830  aomclem6  40884  lmhmfgsplit  40911  hbtlem5  40953  iunrelexpuztr  41327  ismnu  41879  3adantll3  42587  ioondisj2  43031  ioondisj1  43032  iccintsng  43061  icccncfext  43428  stoweidlem61  43602  fourierdlem42  43690  fourierdlem73  43720  smflimlem2  44307  domnmsuppn0  45705  lincresunit3  45822  nnolog2flm1  45936  itschlc0xyqsol1  46112  itschlc0xyqsol  46113