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  6336  f1prex  7284  poxp3  8151  fprlem2  8303  naddsuc2  8695  iunfictbso  10174  fin1a2lem13  10471  prlem934  11099  ifle  13308  ixxlb  13479  elfzonelfzo  13884  swrdcl  14773  subcn2  15742  qexpz  17059  mreexexd  17802  initoeu2lem2  18170  issubmnd  18933  frmdup3lem  19042  pmtrf  19649  pgpssslw  19808  lsmmod  19869  reslmhm2b  21309  lsmcl  21338  lbsextlem3  21418  frlmsslsp  22082  islindf4  22124  coe1mul2  22568  coe1fzgsumdlem  22601  evl1gsumdlem  22654  scmate  22805  mdetdiaglem  22893  madurid  22939  cramerlem2  22986  pmatcollpw3lem  23081  iscnp4  23561  cnrest2  23584  ordthauslem  23681  cncmp  23690  clsconn  23728  rnelfmlem  24251  flimrest  24282  isfcf  24333  cnpfcf  24340  alexsubALT  24350  cldsubg  24410  utop2nei  24549  neipcfilu  24594  blssps  24723  blss  24724  stdbdbl  24816  metcnp3  24839  nmoeq0  25035  xrsxmet  25109  metdseq0  25154  addcnlem  25164  xrhmeo  25247  nmhmcn  25421  cfilres  25597  lgsfcl2  27612  lgsdir  27641  lgsne0  27644  nosupbnd1lem3  28049  nosupbnd1lem4  28050  nosupbnd1lem5  28051  nosupbnd2  28055  noinfbnd1lem3  28064  noinfbnd1lem4  28065  noinfbnd1lem5  28066  noinfbnd2  28070  ltslpss  28276  leadds1  28357  ltmuls2  28539  bdayfinbndlem1  28835  istrkgcb  28900  axcontlem2  29525  axcontlem7  29530  axcontlem8  29531  subupgr  29850  clwwlknonex2  30682  frgr3v  30858  pjhthmo  31886  xrge0adddir  33561  dimvalfi  34216  pcmplfinf  34475  probun  35034  satfv1lem  36096  trisegint  36763  btwnconn1lem13  36834  outsideoftr  36864  outsideofeq  36865  linethru  36888  isbasisrelowllem1  38246  atlatmstc  40344  cvlcvr1  40364  hlrelat  40427  intnatN  40432  cvrval5  40440  2at0mat0  40550  llncvrlpln  40583  lplnexllnN  40589  lplncvrlvol  40641  lncvrelatN  40806  lncmp  40808  paddasslem5  40849  pmapjoin  40877  pmapjat1  40878  pclclN  40916  lhprelat3N  41065  cdleme32fvcl  41465  cdlemg1a  41595  cdlemg1cN  41612  cdlemg39  41741  ltrncom  41763  dihmeetALTN  42352  dihlspsnat  42358  mapdrvallem2  42670  sticksstones12  43176  mzpsubst  43712  lzunuz  43732  acongeq  43943  jm2.19  43953  jm2.27  43968  aomclem6  44019  lmhmfgsplit  44046  hbtlem5  44088  nadd2rabtr  44344  iunrelexpuztr  44678  ismnu  45204  3adantll3  46002  ioondisj2  46449  ioondisj1  46450  iccintsng  46479  icccncfext  46841  stoweidlem61  47015  fourierdlem42  47103  fourierdlem73  47133  smflimlem2  47726  domnmsuppn0  49425  lincresunit3  49537  nnolog2flm1  49646  itschlc0xyqsol1  49822  itschlc0xyqsol  49823