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

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

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 1088

This theorem is referenced by:  frpomin  6316  f1prex  7262  poxp3  8132  fprlem2  8283  naddsuc2  8668  iunfictbso  10074  fin1a2lem13  10372  prlem934  10993  ifle  13164  ixxlb  13335  elfzonelfzo  13737  swrdcl  14617  subcn2  15568  qexpz  16879  mreexexd  17616  initoeu2lem2  17984  issubmnd  18695  frmdup3lem  18800  pmtrf  19392  pgpssslw  19551  lsmmod  19612  reslmhm2b  20968  lsmcl  20997  lbsextlem3  21077  frlmsslsp  21712  islindf4  21754  coe1mul2  22162  coe1fzgsumdlem  22197  evl1gsumdlem  22250  scmate  22404  mdetdiaglem  22492  madurid  22538  cramerlem2  22582  pmatcollpw3lem  22677  iscnp4  23157  cnrest2  23180  ordthauslem  23277  cncmp  23286  clsconn  23324  rnelfmlem  23846  flimrest  23877  isfcf  23928  cnpfcf  23935  alexsubALT  23945  cldsubg  24005  utop2nei  24145  neipcfilu  24190  blssps  24319  blss  24320  stdbdbl  24412  metcnp3  24435  nmoeq0  24631  xrsxmet  24705  metdseq0  24750  addcnlem  24760  xrhmeo  24851  nmhmcn  25027  cfilres  25203  lgsfcl2  27221  lgsdir  27250  lgsne0  27253  nosupbnd1lem3  27629  nosupbnd1lem4  27630  nosupbnd1lem5  27631  nosupbnd2  27635  noinfbnd1lem3  27644  noinfbnd1lem4  27645  noinfbnd1lem5  27646  noinfbnd2  27650  sltlpss  27826  sleadd1  27903  sltmul2  28081  istrkgcb  28390  axcontlem2  28899  axcontlem7  28904  axcontlem8  28905  subupgr  29221  clwwlknonex2  30045  frgr3v  30211  pjhthmo  31238  xrge0adddir  32966  dimvalfi  33604  pcmplfinf  33858  probun  34417  satfv1lem  35356  trisegint  36023  btwnconn1lem13  36094  outsideoftr  36124  outsideofeq  36125  linethru  36148  isbasisrelowllem1  37350  atlatmstc  39319  cvlcvr1  39339  hlrelat  39403  intnatN  39408  cvrval5  39416  2at0mat0  39526  llncvrlpln  39559  lplnexllnN  39565  lplncvrlvol  39617  lncvrelatN  39782  lncmp  39784  paddasslem5  39825  pmapjoin  39853  pmapjat1  39854  pclclN  39892  lhprelat3N  40041  cdleme32fvcl  40441  cdlemg1a  40571  cdlemg1cN  40588  cdlemg39  40717  ltrncom  40739  dihmeetALTN  41328  dihlspsnat  41334  mapdrvallem2  41646  sticksstones12  42153  mzpsubst  42743  lzunuz  42763  acongeq  42979  jm2.19  42989  jm2.27  43004  aomclem6  43055  lmhmfgsplit  43082  hbtlem5  43124  nadd2rabtr  43380  iunrelexpuztr  43715  ismnu  44257  3adantll3  45043  ioondisj2  45498  ioondisj1  45499  iccintsng  45528  icccncfext  45892  stoweidlem61  46066  fourierdlem42  46154  fourierdlem73  46184  smflimlem2  46777  domnmsuppn0  48361  lincresunit3  48474  nnolog2flm1  48583  itschlc0xyqsol1  48759  itschlc0xyqsol  48760