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  6298  f1prex  7232  poxp3  8093  fprlem2  8244  naddsuc2  8630  iunfictbso  10027  fin1a2lem13  10325  prlem934  10947  ifle  13140  ixxlb  13311  elfzonelfzo  13715  swrdcl  14599  subcn2  15548  qexpz  16863  mreexexd  17605  initoeu2lem2  17973  issubmnd  18720  frmdup3lem  18825  pmtrf  19421  pgpssslw  19580  lsmmod  19641  reslmhm2b  21041  lsmcl  21070  lbsextlem3  21150  frlmsslsp  21786  islindf4  21828  coe1mul2  22244  coe1fzgsumdlem  22278  evl1gsumdlem  22331  scmate  22485  mdetdiaglem  22573  madurid  22619  cramerlem2  22663  pmatcollpw3lem  22758  iscnp4  23238  cnrest2  23261  ordthauslem  23358  cncmp  23367  clsconn  23405  rnelfmlem  23927  flimrest  23958  isfcf  24009  cnpfcf  24016  alexsubALT  24026  cldsubg  24086  utop2nei  24225  neipcfilu  24270  blssps  24399  blss  24400  stdbdbl  24492  metcnp3  24515  nmoeq0  24711  xrsxmet  24785  metdseq0  24830  addcnlem  24840  xrhmeo  24923  nmhmcn  25097  cfilres  25273  lgsfcl2  27280  lgsdir  27309  lgsne0  27312  nosupbnd1lem3  27688  nosupbnd1lem4  27689  nosupbnd1lem5  27690  nosupbnd2  27694  noinfbnd1lem3  27703  noinfbnd1lem4  27704  noinfbnd1lem5  27705  noinfbnd2  27709  ltslpss  27914  leadds1  27995  ltmuls2  28177  bdayfinbndlem1  28473  istrkgcb  28538  axcontlem2  29048  axcontlem7  29053  axcontlem8  29054  subupgr  29370  clwwlknonex2  30194  frgr3v  30360  pjhthmo  31388  xrge0adddir  33093  dimvalfi  33761  pcmplfinf  34021  probun  34579  satfv1lem  35560  trisegint  36226  btwnconn1lem13  36297  outsideoftr  36327  outsideofeq  36328  linethru  36351  isbasisrelowllem1  37685  atlatmstc  39779  cvlcvr1  39799  hlrelat  39862  intnatN  39867  cvrval5  39875  2at0mat0  39985  llncvrlpln  40018  lplnexllnN  40024  lplncvrlvol  40076  lncvrelatN  40241  lncmp  40243  paddasslem5  40284  pmapjoin  40312  pmapjat1  40313  pclclN  40351  lhprelat3N  40500  cdleme32fvcl  40900  cdlemg1a  41030  cdlemg1cN  41047  cdlemg39  41176  ltrncom  41198  dihmeetALTN  41787  dihlspsnat  41793  mapdrvallem2  42105  sticksstones12  42611  mzpsubst  43194  lzunuz  43214  acongeq  43429  jm2.19  43439  jm2.27  43454  aomclem6  43505  lmhmfgsplit  43532  hbtlem5  43574  nadd2rabtr  43830  iunrelexpuztr  44164  ismnu  44706  3adantll3  45491  ioondisj2  45941  ioondisj1  45942  iccintsng  45971  icccncfext  46333  stoweidlem61  46507  fourierdlem42  46595  fourierdlem73  46625  smflimlem2  47218  domnmsuppn0  48857  lincresunit3  48969  nnolog2flm1  49078  itschlc0xyqsol1  49254  itschlc0xyqsol  49255