Theorem simpll2 1220

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  frpomin  6298  f1prex  7235  poxp3  8097  fprlem2  8248  naddsuc2  8634  iunfictbso  10034  fin1a2lem13  10332  prlem934  10954  ifle  13147  ixxlb  13318  elfzonelfzo  13722  swrdcl  14606  subcn2  15555  qexpz  16870  mreexexd  17612  initoeu2lem2  17980  issubmnd  18727  frmdup3lem  18832  pmtrf  19428  pgpssslw  19587  lsmmod  19648  reslmhm2b  21051  lsmcl  21080  lbsextlem3  21160  frlmsslsp  21778  islindf4  21820  coe1mul2  22262  coe1fzgsumdlem  22296  evl1gsumdlem  22349  scmate  22500  mdetdiaglem  22588  madurid  22634  cramerlem2  22678  pmatcollpw3lem  22773  iscnp4  23253  cnrest2  23276  ordthauslem  23373  cncmp  23382  clsconn  23420  rnelfmlem  23942  flimrest  23973  isfcf  24024  cnpfcf  24031  alexsubALT  24041  cldsubg  24101  utop2nei  24240  neipcfilu  24285  blssps  24414  blss  24415  stdbdbl  24507  metcnp3  24530  nmoeq0  24726  xrsxmet  24800  metdseq0  24845  addcnlem  24855  xrhmeo  24938  nmhmcn  25112  cfilres  25288  lgsfcl2  27291  lgsdir  27320  lgsne0  27323  nosupbnd1lem3  27699  nosupbnd1lem4  27700  nosupbnd1lem5  27701  nosupbnd2  27705  noinfbnd1lem3  27714  noinfbnd1lem4  27715  noinfbnd1lem5  27716  noinfbnd2  27720  ltslpss  27925  leadds1  28006  ltmuls2  28188  bdayfinbndlem1  28484  istrkgcb  28549  axcontlem2  29059  axcontlem7  29064  axcontlem8  29065  subupgr  29381  clwwlknonex2  30204  frgr3v  30370  pjhthmo  31398  xrge0adddir  33104  dimvalfi  33793  pcmplfinf  34052  probun  34610  satfv1lem  35597  trisegint  36263  btwnconn1lem13  36334  outsideoftr  36364  outsideofeq  36365  linethru  36388  isbasisrelowllem1  37724  atlatmstc  39818  cvlcvr1  39838  hlrelat  39901  intnatN  39906  cvrval5  39914  2at0mat0  40024  llncvrlpln  40057  lplnexllnN  40063  lplncvrlvol  40115  lncvrelatN  40280  lncmp  40282  paddasslem5  40323  pmapjoin  40351  pmapjat1  40352  pclclN  40390  lhprelat3N  40539  cdleme32fvcl  40939  cdlemg1a  41069  cdlemg1cN  41086  cdlemg39  41215  ltrncom  41237  dihmeetALTN  41826  dihlspsnat  41832  mapdrvallem2  42144  sticksstones12  42650  mzpsubst  43204  lzunuz  43224  acongeq  43435  jm2.19  43445  jm2.27  43460  aomclem6  43511  lmhmfgsplit  43538  hbtlem5  43580  nadd2rabtr  43836  iunrelexpuztr  44170  ismnu  44712  3adantll3  45497  ioondisj2  45945  ioondisj1  45946  iccintsng  45975  icccncfext  46337  stoweidlem61  46511  fourierdlem42  46599  fourierdlem73  46629  smflimlem2  47222  domnmsuppn0  48867  lincresunit3  48979  nnolog2flm1  49088  itschlc0xyqsol1  49264  itschlc0xyqsol  49265