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  6329  f1prex  7277  poxp3  8149  fprlem2  8300  naddsuc2  8713  iunfictbso  10128  fin1a2lem13  10426  prlem934  11047  ifle  13213  ixxlb  13384  elfzonelfzo  13785  swrdcl  14663  subcn2  15611  qexpz  16921  mreexexd  17660  initoeu2lem2  18028  issubmnd  18739  frmdup3lem  18844  pmtrf  19436  pgpssslw  19595  lsmmod  19656  reslmhm2b  21012  lsmcl  21041  lbsextlem3  21121  frlmsslsp  21756  islindf4  21798  coe1mul2  22206  coe1fzgsumdlem  22241  evl1gsumdlem  22294  scmate  22448  mdetdiaglem  22536  madurid  22582  cramerlem2  22626  pmatcollpw3lem  22721  iscnp4  23201  cnrest2  23224  ordthauslem  23321  cncmp  23330  clsconn  23368  rnelfmlem  23890  flimrest  23921  isfcf  23972  cnpfcf  23979  alexsubALT  23989  cldsubg  24049  utop2nei  24189  neipcfilu  24234  blssps  24363  blss  24364  stdbdbl  24456  metcnp3  24479  nmoeq0  24675  xrsxmet  24749  metdseq0  24794  addcnlem  24804  xrhmeo  24895  nmhmcn  25071  cfilres  25248  lgsfcl2  27266  lgsdir  27295  lgsne0  27298  nosupbnd1lem3  27674  nosupbnd1lem4  27675  nosupbnd1lem5  27676  nosupbnd2  27680  noinfbnd1lem3  27689  noinfbnd1lem4  27690  noinfbnd1lem5  27691  noinfbnd2  27695  sltlpss  27871  sleadd1  27948  sltmul2  28126  istrkgcb  28435  axcontlem2  28944  axcontlem7  28949  axcontlem8  28950  subupgr  29266  clwwlknonex2  30090  frgr3v  30256  pjhthmo  31283  xrge0adddir  33013  dimvalfi  33641  pcmplfinf  33892  probun  34451  satfv1lem  35384  trisegint  36046  btwnconn1lem13  36117  outsideoftr  36147  outsideofeq  36148  linethru  36171  isbasisrelowllem1  37373  atlatmstc  39337  cvlcvr1  39357  hlrelat  39421  intnatN  39426  cvrval5  39434  2at0mat0  39544  llncvrlpln  39577  lplnexllnN  39583  lplncvrlvol  39635  lncvrelatN  39800  lncmp  39802  paddasslem5  39843  pmapjoin  39871  pmapjat1  39872  pclclN  39910  lhprelat3N  40059  cdleme32fvcl  40459  cdlemg1a  40589  cdlemg1cN  40606  cdlemg39  40735  ltrncom  40757  dihmeetALTN  41346  dihlspsnat  41352  mapdrvallem2  41664  sticksstones12  42171  mzpsubst  42771  lzunuz  42791  acongeq  43007  jm2.19  43017  jm2.27  43032  aomclem6  43083  lmhmfgsplit  43110  hbtlem5  43152  nadd2rabtr  43408  iunrelexpuztr  43743  ismnu  44285  3adantll3  45066  ioondisj2  45522  ioondisj1  45523  iccintsng  45552  icccncfext  45916  stoweidlem61  46090  fourierdlem42  46178  fourierdlem73  46208  smflimlem2  46801  domnmsuppn0  48344  lincresunit3  48457  nnolog2flm1  48570  itschlc0xyqsol1  48746  itschlc0xyqsol  48747