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  6306  f1prex  7240  poxp3  8102  fprlem2  8253  naddsuc2  8639  iunfictbso  10036  fin1a2lem13  10334  prlem934  10956  ifle  13124  ixxlb  13295  elfzonelfzo  13697  swrdcl  14581  subcn2  15530  qexpz  16841  mreexexd  17583  initoeu2lem2  17951  issubmnd  18698  frmdup3lem  18803  pmtrf  19396  pgpssslw  19555  lsmmod  19616  reslmhm2b  21018  lsmcl  21047  lbsextlem3  21127  frlmsslsp  21763  islindf4  21805  coe1mul2  22223  coe1fzgsumdlem  22259  evl1gsumdlem  22312  scmate  22466  mdetdiaglem  22554  madurid  22600  cramerlem2  22644  pmatcollpw3lem  22739  iscnp4  23219  cnrest2  23242  ordthauslem  23339  cncmp  23348  clsconn  23386  rnelfmlem  23908  flimrest  23939  isfcf  23990  cnpfcf  23997  alexsubALT  24007  cldsubg  24067  utop2nei  24206  neipcfilu  24251  blssps  24380  blss  24381  stdbdbl  24473  metcnp3  24496  nmoeq0  24692  xrsxmet  24766  metdseq0  24811  addcnlem  24821  xrhmeo  24912  nmhmcn  25088  cfilres  25264  lgsfcl2  27282  lgsdir  27311  lgsne0  27314  nosupbnd1lem3  27690  nosupbnd1lem4  27691  nosupbnd1lem5  27692  nosupbnd2  27696  noinfbnd1lem3  27705  noinfbnd1lem4  27706  noinfbnd1lem5  27707  noinfbnd2  27711  ltslpss  27916  leadds1  27997  ltmuls2  28179  bdayfinbndlem1  28475  istrkgcb  28540  axcontlem2  29050  axcontlem7  29055  axcontlem8  29056  subupgr  29372  clwwlknonex2  30196  frgr3v  30362  pjhthmo  31389  xrge0adddir  33110  dimvalfi  33778  pcmplfinf  34038  probun  34596  satfv1lem  35575  trisegint  36241  btwnconn1lem13  36312  outsideoftr  36342  outsideofeq  36343  linethru  36366  isbasisrelowllem1  37604  atlatmstc  39689  cvlcvr1  39709  hlrelat  39772  intnatN  39777  cvrval5  39785  2at0mat0  39895  llncvrlpln  39928  lplnexllnN  39934  lplncvrlvol  39986  lncvrelatN  40151  lncmp  40153  paddasslem5  40194  pmapjoin  40222  pmapjat1  40223  pclclN  40261  lhprelat3N  40410  cdleme32fvcl  40810  cdlemg1a  40940  cdlemg1cN  40957  cdlemg39  41086  ltrncom  41108  dihmeetALTN  41697  dihlspsnat  41703  mapdrvallem2  42015  sticksstones12  42522  mzpsubst  43099  lzunuz  43119  acongeq  43334  jm2.19  43344  jm2.27  43359  aomclem6  43410  lmhmfgsplit  43437  hbtlem5  43479  nadd2rabtr  43735  iunrelexpuztr  44069  ismnu  44611  3adantll3  45396  ioondisj2  45847  ioondisj1  45848  iccintsng  45877  icccncfext  46239  stoweidlem61  46413  fourierdlem42  46501  fourierdlem73  46531  smflimlem2  47124  domnmsuppn0  48723  lincresunit3  48835  nnolog2flm1  48944  itschlc0xyqsol1  49120  itschlc0xyqsol  49121