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  6364  f1prex  7318  poxp3  8197  fprlem2  8350  naddsuc2  8742  iunfictbso  10223  fin1a2lem13  10520  prlem934  11148  ifle  13357  ixxlb  13528  elfzonelfzo  13934  swrdcl  14824  subcn2  15794  qexpz  17111  mreexexd  17854  initoeu2lem2  18222  issubmnd  18985  frmdup3lem  19094  pmtrf  19702  pgpssslw  19861  lsmmod  19922  reslmhm2b  21362  lsmcl  21391  lbsextlem3  21471  frlmsslsp  22135  islindf4  22177  coe1mul2  22621  coe1fzgsumdlem  22654  evl1gsumdlem  22707  scmate  22858  mdetdiaglem  22946  madurid  22992  cramerlem2  23039  pmatcollpw3lem  23134  iscnp4  23614  cnrest2  23637  ordthauslem  23734  cncmp  23743  clsconn  23781  rnelfmlem  24304  flimrest  24335  isfcf  24386  cnpfcf  24393  alexsubALT  24403  cldsubg  24463  utop2nei  24602  neipcfilu  24647  blssps  24776  blss  24777  stdbdbl  24869  metcnp3  24892  nmoeq0  25088  xrsxmet  25162  metdseq0  25207  addcnlem  25217  xrhmeo  25300  nmhmcn  25474  cfilres  25650  lgsfcl2  27663  lgsdir  27692  lgsne0  27695  nosupbnd1lem3  28100  nosupbnd1lem4  28101  nosupbnd1lem5  28102  nosupbnd2  28106  noinfbnd1lem3  28115  noinfbnd1lem4  28116  noinfbnd1lem5  28117  noinfbnd2  28121  ltslpss  28327  leadds1  28408  ltmuls2  28590  bdayfinbndlem1  28886  istrkgcb  28951  axcontlem2  29576  axcontlem7  29581  axcontlem8  29582  subupgr  29901  clwwlknonex2  30733  frgr3v  30909  pjhthmo  31937  xrge0adddir  33655  dimvalfi  34317  pcmplfinf  34576  probun  35134  satfv1lem  36307  trisegint  36984  btwnconn1lem13  37055  outsideoftr  37085  outsideofeq  37086  linethru  37109  isbasisrelowllem1  38483  atlatmstc  40579  cvlcvr1  40599  hlrelat  40662  intnatN  40667  cvrval5  40675  2at0mat0  40785  llncvrlpln  40818  lplnexllnN  40824  lplncvrlvol  40876  lncvrelatN  41041  lncmp  41043  paddasslem5  41084  pmapjoin  41112  pmapjat1  41113  pclclN  41151  lhprelat3N  41300  cdleme32fvcl  41700  cdlemg1a  41830  cdlemg1cN  41847  cdlemg39  41976  ltrncom  41998  dihmeetALTN  42587  dihlspsnat  42593  mapdrvallem2  42905  sticksstones12  43411  mzpsubst  43963  lzunuz  43983  acongeq  44194  jm2.19  44204  jm2.27  44219  aomclem6  44265  lmhmfgsplit  44292  hbtlem5  44333  nadd2rabtr  44589  iunrelexpuztr  44922  ismnu  45448  3adantll3  46275  ioondisj2  46720  ioondisj1  46721  iccintsng  46750  icccncfext  47112  stoweidlem61  47286  fourierdlem42  47374  fourierdlem73  47404  smflimlem2  47997  domnmsuppn0  49696  lincresunit3  49808  nnolog2flm1  49917  itschlc0xyqsol1  50093  itschlc0xyqsol  50094