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  6343  f1prex  7292  poxp3  8169  fprlem2  8322  naddsuc2  8714  iunfictbso  10196  fin1a2lem13  10493  prlem934  11121  ifle  13330  ixxlb  13501  elfzonelfzo  13907  swrdcl  14797  subcn2  15767  qexpz  17084  mreexexd  17827  initoeu2lem2  18195  issubmnd  18958  frmdup3lem  19067  pmtrf  19674  pgpssslw  19833  lsmmod  19894  reslmhm2b  21334  lsmcl  21363  lbsextlem3  21443  frlmsslsp  22107  islindf4  22149  coe1mul2  22593  coe1fzgsumdlem  22626  evl1gsumdlem  22679  scmate  22830  mdetdiaglem  22918  madurid  22964  cramerlem2  23011  pmatcollpw3lem  23106  iscnp4  23586  cnrest2  23609  ordthauslem  23706  cncmp  23715  clsconn  23753  rnelfmlem  24276  flimrest  24307  isfcf  24358  cnpfcf  24365  alexsubALT  24375  cldsubg  24435  utop2nei  24574  neipcfilu  24619  blssps  24748  blss  24749  stdbdbl  24841  metcnp3  24864  nmoeq0  25060  xrsxmet  25134  metdseq0  25179  addcnlem  25189  xrhmeo  25272  nmhmcn  25446  cfilres  25622  lgsfcl2  27635  lgsdir  27664  lgsne0  27667  nosupbnd1lem3  28072  nosupbnd1lem4  28073  nosupbnd1lem5  28074  nosupbnd2  28078  noinfbnd1lem3  28087  noinfbnd1lem4  28088  noinfbnd1lem5  28089  noinfbnd2  28093  ltslpss  28299  leadds1  28380  ltmuls2  28562  bdayfinbndlem1  28858  istrkgcb  28923  axcontlem2  29548  axcontlem7  29553  axcontlem8  29554  subupgr  29873  clwwlknonex2  30705  frgr3v  30881  pjhthmo  31909  xrge0adddir  33625  dimvalfi  34280  pcmplfinf  34539  probun  35097  satfv1lem  36213  trisegint  36885  btwnconn1lem13  36956  outsideoftr  36986  outsideofeq  36987  linethru  37010  isbasisrelowllem1  38371  atlatmstc  40469  cvlcvr1  40489  hlrelat  40552  intnatN  40557  cvrval5  40565  2at0mat0  40675  llncvrlpln  40708  lplnexllnN  40714  lplncvrlvol  40766  lncvrelatN  40931  lncmp  40933  paddasslem5  40974  pmapjoin  41002  pmapjat1  41003  pclclN  41041  lhprelat3N  41190  cdleme32fvcl  41590  cdlemg1a  41720  cdlemg1cN  41737  cdlemg39  41866  ltrncom  41888  dihmeetALTN  42477  dihlspsnat  42483  mapdrvallem2  42795  sticksstones12  43301  mzpsubst  43852  lzunuz  43872  acongeq  44083  jm2.19  44093  jm2.27  44108  aomclem6  44154  lmhmfgsplit  44181  hbtlem5  44223  nadd2rabtr  44479  iunrelexpuztr  44812  ismnu  45338  3adantll3  46152  ioondisj2  46598  ioondisj1  46599  iccintsng  46628  icccncfext  46990  stoweidlem61  47164  fourierdlem42  47252  fourierdlem73  47282  smflimlem2  47875  domnmsuppn0  49574  lincresunit3  49686  nnolog2flm1  49795  itschlc0xyqsol1  49971  itschlc0xyqsol  49972