Theorem simpll2 1214

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

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1088

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 398  df-3an 1090

This theorem is referenced by:  frpomin  6342  f1prex  7282  poxp3  8136  fprlem2  8286  iunfictbso  10109  fin1a2lem13  10407  prlem934  11028  ifle  13176  ixxlb  13346  elfzonelfzo  13734  swrdcl  14595  subcn2  15539  qexpz  16834  mreexexd  17592  initoeu2lem2  17965  issubmnd  18652  frmdup3lem  18747  pmtrf  19323  pgpssslw  19482  lsmmod  19543  reslmhm2b  20665  lsmcl  20694  lbsextlem3  20773  frlmsslsp  21351  islindf4  21393  coe1mul2  21791  coe1fzgsumdlem  21825  evl1gsumdlem  21875  scmate  22012  mdetdiaglem  22100  madurid  22146  cramerlem2  22190  pmatcollpw3lem  22285  iscnp4  22767  cnrest2  22790  ordthauslem  22887  cncmp  22896  clsconn  22934  rnelfmlem  23456  flimrest  23487  isfcf  23538  cnpfcf  23545  alexsubALT  23555  cldsubg  23615  utop2nei  23755  neipcfilu  23801  blssps  23930  blss  23931  stdbdbl  24026  metcnp3  24049  nmoeq0  24253  xrsxmet  24325  metdseq0  24370  addcnlem  24380  xrhmeo  24462  nmhmcn  24636  cfilres  24813  lgsfcl2  26806  lgsdir  26835  lgsne0  26838  nosupbnd1lem3  27213  nosupbnd1lem4  27214  nosupbnd1lem5  27215  nosupbnd2  27219  noinfbnd1lem3  27228  noinfbnd1lem4  27229  noinfbnd1lem5  27230  noinfbnd2  27234  sltlpss  27402  sleadd1  27475  sltmul2  27626  istrkgcb  27738  axcontlem2  28254  axcontlem7  28259  axcontlem8  28260  subupgr  28575  clwwlknonex2  29393  frgr3v  29559  pjhthmo  30586  xrge0adddir  32224  dimvalfi  32718  pcmplfinf  32872  probun  33449  satfv1lem  34384  trisegint  35031  btwnconn1lem13  35102  outsideoftr  35132  outsideofeq  35133  linethru  35156  isbasisrelowllem1  36284  atlatmstc  38237  cvlcvr1  38257  hlrelat  38321  intnatN  38326  cvrval5  38334  2at0mat0  38444  llncvrlpln  38477  lplnexllnN  38483  lplncvrlvol  38535  lncvrelatN  38700  lncmp  38702  paddasslem5  38743  pmapjoin  38771  pmapjat1  38772  pclclN  38810  lhprelat3N  38959  cdleme32fvcl  39359  cdlemg1a  39489  cdlemg1cN  39506  cdlemg39  39635  ltrncom  39657  dihmeetALTN  40246  dihlspsnat  40252  mapdrvallem2  40564  sticksstones12  41022  mzpsubst  41534  lzunuz  41554  acongeq  41770  jm2.19  41780  jm2.27  41795  aomclem6  41849  lmhmfgsplit  41876  hbtlem5  41918  nadd2rabtr  42182  naddsuc2  42191  iunrelexpuztr  42518  ismnu  43068  3adantll3  43774  ioondisj2  44254  ioondisj1  44255  iccintsng  44284  icccncfext  44651  stoweidlem61  44825  fourierdlem42  44913  fourierdlem73  44943  smflimlem2  45536  domnmsuppn0  47093  lincresunit3  47210  nnolog2flm1  47324  itschlc0xyqsol1  47500  itschlc0xyqsol  47501