Theorem simpll2 1215

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  frpomin  6304  f1prex  7239  poxp3  8100  fprlem2  8251  naddsuc2  8637  iunfictbso  10036  fin1a2lem13  10334  prlem934  10956  ifle  13149  ixxlb  13320  elfzonelfzo  13724  swrdcl  14608  subcn2  15557  qexpz  16872  mreexexd  17614  initoeu2lem2  17982  issubmnd  18729  frmdup3lem  18834  pmtrf  19430  pgpssslw  19589  lsmmod  19650  reslmhm2b  21049  lsmcl  21078  lbsextlem3  21158  frlmsslsp  21776  islindf4  21818  coe1mul2  22234  coe1fzgsumdlem  22268  evl1gsumdlem  22321  scmate  22475  mdetdiaglem  22563  madurid  22609  cramerlem2  22653  pmatcollpw3lem  22748  iscnp4  23228  cnrest2  23251  ordthauslem  23348  cncmp  23357  clsconn  23395  rnelfmlem  23917  flimrest  23948  isfcf  23999  cnpfcf  24006  alexsubALT  24016  cldsubg  24076  utop2nei  24215  neipcfilu  24260  blssps  24389  blss  24390  stdbdbl  24482  metcnp3  24505  nmoeq0  24701  xrsxmet  24775  metdseq0  24820  addcnlem  24830  xrhmeo  24913  nmhmcn  25087  cfilres  25263  lgsfcl2  27266  lgsdir  27295  lgsne0  27298  nosupbnd1lem3  27674  nosupbnd1lem4  27675  nosupbnd1lem5  27676  nosupbnd2  27680  noinfbnd1lem3  27689  noinfbnd1lem4  27690  noinfbnd1lem5  27691  noinfbnd2  27695  ltslpss  27900  leadds1  27981  ltmuls2  28163  bdayfinbndlem1  28459  istrkgcb  28524  axcontlem2  29034  axcontlem7  29039  axcontlem8  29040  subupgr  29356  clwwlknonex2  30179  frgr3v  30345  pjhthmo  31373  xrge0adddir  33078  dimvalfi  33746  pcmplfinf  34005  probun  34563  satfv1lem  35544  trisegint  36210  btwnconn1lem13  36281  outsideoftr  36311  outsideofeq  36312  linethru  36335  isbasisrelowllem1  37671  atlatmstc  39765  cvlcvr1  39785  hlrelat  39848  intnatN  39853  cvrval5  39861  2at0mat0  39971  llncvrlpln  40004  lplnexllnN  40010  lplncvrlvol  40062  lncvrelatN  40227  lncmp  40229  paddasslem5  40270  pmapjoin  40298  pmapjat1  40299  pclclN  40337  lhprelat3N  40486  cdleme32fvcl  40886  cdlemg1a  41016  cdlemg1cN  41033  cdlemg39  41162  ltrncom  41184  dihmeetALTN  41773  dihlspsnat  41779  mapdrvallem2  42091  sticksstones12  42597  mzpsubst  43180  lzunuz  43200  acongeq  43411  jm2.19  43421  jm2.27  43436  aomclem6  43487  lmhmfgsplit  43514  hbtlem5  43556  nadd2rabtr  43812  iunrelexpuztr  44146  ismnu  44688  3adantll3  45473  ioondisj2  45923  ioondisj1  45924  iccintsng  45953  icccncfext  46315  stoweidlem61  46489  fourierdlem42  46577  fourierdlem73  46607  smflimlem2  47200  domnmsuppn0  48845  lincresunit3  48957  nnolog2flm1  49066  itschlc0xyqsol1  49242  itschlc0xyqsol  49243