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 739	1 ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  frpomin  6348  f1prex  7293  poxp3  8155  fprlem2  8307  naddsuc2  8697  iunfictbso  10117  fin1a2lem13  10414  prlem934  11036  ifle  13241  ixxlb  13412  elfzonelfzo  13817  swrdcl  14705  subcn2  15672  qexpz  16986  mreexexd  17729  initoeu2lem2  18097  issubmnd  18848  frmdup3lem  18956  pmtrf  19556  pgpssslw  19715  lsmmod  19776  reslmhm2b  21212  lsmcl  21241  lbsextlem3  21321  frlmsslsp  21983  islindf4  22025  coe1mul2  22467  coe1fzgsumdlem  22500  evl1gsumdlem  22553  scmate  22704  mdetdiaglem  22792  madurid  22838  cramerlem2  22882  pmatcollpw3lem  22977  iscnp4  23457  cnrest2  23480  ordthauslem  23577  cncmp  23586  clsconn  23624  rnelfmlem  24146  flimrest  24177  isfcf  24228  cnpfcf  24235  alexsubALT  24245  cldsubg  24305  utop2nei  24444  neipcfilu  24489  blssps  24618  blss  24619  stdbdbl  24711  metcnp3  24734  nmoeq0  24930  xrsxmet  25004  metdseq0  25049  addcnlem  25059  xrhmeo  25142  nmhmcn  25316  cfilres  25492  lgsfcl2  27504  lgsdir  27533  lgsne0  27536  nosupbnd1lem3  27911  nosupbnd1lem4  27912  nosupbnd1lem5  27913  nosupbnd2  27917  noinfbnd1lem3  27926  noinfbnd1lem4  27927  noinfbnd1lem5  27928  noinfbnd2  27932  ltslpss  28138  leadds1  28219  ltmuls2  28401  bdayfinbndlem1  28697  istrkgcb  28762  axcontlem2  29352  axcontlem7  29357  axcontlem8  29358  subupgr  29674  clwwlknonex2  30497  frgr3v  30663  pjhthmo  31691  xrge0adddir  33369  dimvalfi  34023  pcmplfinf  34282  probun  34841  satfv1lem  35875  trisegint  36541  btwnconn1lem13  36612  outsideoftr  36642  outsideofeq  36643  linethru  36666  isbasisrelowllem1  38042  atlatmstc  40134  cvlcvr1  40154  hlrelat  40217  intnatN  40222  cvrval5  40230  2at0mat0  40340  llncvrlpln  40373  lplnexllnN  40379  lplncvrlvol  40431  lncvrelatN  40596  lncmp  40598  paddasslem5  40639  pmapjoin  40667  pmapjat1  40668  pclclN  40706  lhprelat3N  40855  cdleme32fvcl  41255  cdlemg1a  41385  cdlemg1cN  41402  cdlemg39  41531  ltrncom  41553  dihmeetALTN  42142  dihlspsnat  42148  mapdrvallem2  42460  sticksstones12  42966  mzpsubst  43520  lzunuz  43540  acongeq  43751  jm2.19  43761  jm2.27  43776  aomclem6  43827  lmhmfgsplit  43854  hbtlem5  43896  nadd2rabtr  44152  iunrelexpuztr  44486  ismnu  45012  3adantll3  45803  ioondisj2  46250  ioondisj1  46251  iccintsng  46280  icccncfext  46642  stoweidlem61  46816  fourierdlem42  46904  fourierdlem73  46934  smflimlem2  47527  domnmsuppn0  49190  lincresunit3  49302  nnolog2flm1  49411  itschlc0xyqsol1  49587  itschlc0xyqsol  49588