Theorem simpll2 1277

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

Syntax hints:   → wi 4   ∧ wa 386   ∧ w3a 1113

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 199  df-an 387  df-3an 1115

This theorem is referenced by:  f1prex  6795  wemappo  8724  iunfictbso  9251  fin1a2lem13  9550  prlem934  10171  ifle  12317  ixxlb  12486  elfzonelfzo  12866  swrdcl  13706  subcn2  14703  qexpz  15977  mreexexd  16662  initoeu2lem2  17018  issubmnd  17672  gsumccat  17732  frmdup3lem  17758  pmtrf  18226  pgpssslw  18381  lsmmod  18440  reslmhm2b  19414  lsmcl  19443  lbsextlem3  19522  coe1mul2  20000  coe1fzgsumdlem  20032  evl1gsumdlem  20081  frlmsslsp  20503  islindf4  20545  scmate  20685  mdetdiaglem  20773  madurid  20819  cramerlem2  20865  pmatcollpw3lem  20959  iscnp4  21439  cnrest2  21462  ordthauslem  21559  cncmp  21567  clsconn  21605  rnelfmlem  22127  flimrest  22158  isfcf  22209  cnpfcf  22216  alexsubALT  22226  cldsubg  22285  utop2nei  22425  neipcfilu  22471  blssps  22600  blss  22601  stdbdbl  22693  metcnp3  22716  nmoeq0  22911  xrsxmet  22983  metdseq0  23028  addcnlem  23038  xrhmeo  23116  nmhmcn  23290  cfilres  23465  lgsfcl2  25442  lgsdir  25471  lgsne0  25474  istrkgcb  25769  axcontlem2  26265  axcontlem7  26270  axcontlem8  26271  subupgr  26585  clwwlknonex2  27485  frgr3v  27657  pjhthmo  28717  xrge0adddir  30238  pcmplfinf  30474  probun  31028  frpomin  32278  nosupbnd1lem3  32396  nosupbnd1lem4  32397  nosupbnd1lem5  32398  nosupbnd2  32402  trisegint  32675  btwnconn1lem13  32746  outsideoftr  32776  outsideofeq  32777  linethru  32800  isbasisrelowllem1  33749  atlatmstc  35395  cvlcvr1  35415  hlrelat  35478  intnatN  35483  cvrval5  35491  2at0mat0  35601  llncvrlpln  35634  lplnexllnN  35640  lplncvrlvol  35692  lncvrelatN  35857  lncmp  35859  paddasslem5  35900  pmapjoin  35928  pmapjat1  35929  pclclN  35967  lhprelat3N  36116  cdleme32fvcl  36516  cdlemg1a  36646  cdlemg1cN  36663  cdlemg39  36792  ltrncom  36814  dihmeetALTN  37403  dihlspsnat  37409  mapdrvallem2  37721  mzpsubst  38156  lzunuz  38176  acongeq  38394  jm2.19  38404  jm2.27  38419  aomclem6  38473  lmhmfgsplit  38500  hbtlem5  38542  iunrelexpuztr  38853  3adantll3  40022  ioondisj2  40514  ioondisj1  40515  iccintsng  40546  icccncfext  40896  stoweidlem61  41073  fourierdlem42  41161  fourierdlem73  41191  smflimlem2  41775  domnmsuppn0  42998  lincresunit3  43118  nnolog2flm1  43232