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  6313  f1prex  7259  poxp3  8129  fprlem2  8280  naddsuc2  8665  iunfictbso  10067  fin1a2lem13  10365  prlem934  10986  ifle  13157  ixxlb  13328  elfzonelfzo  13730  swrdcl  14610  subcn2  15561  qexpz  16872  mreexexd  17609  initoeu2lem2  17977  issubmnd  18688  frmdup3lem  18793  pmtrf  19385  pgpssslw  19544  lsmmod  19605  reslmhm2b  20961  lsmcl  20990  lbsextlem3  21070  frlmsslsp  21705  islindf4  21747  coe1mul2  22155  coe1fzgsumdlem  22190  evl1gsumdlem  22243  scmate  22397  mdetdiaglem  22485  madurid  22531  cramerlem2  22575  pmatcollpw3lem  22670  iscnp4  23150  cnrest2  23173  ordthauslem  23270  cncmp  23279  clsconn  23317  rnelfmlem  23839  flimrest  23870  isfcf  23921  cnpfcf  23928  alexsubALT  23938  cldsubg  23998  utop2nei  24138  neipcfilu  24183  blssps  24312  blss  24313  stdbdbl  24405  metcnp3  24428  nmoeq0  24624  xrsxmet  24698  metdseq0  24743  addcnlem  24753  xrhmeo  24844  nmhmcn  25020  cfilres  25196  lgsfcl2  27214  lgsdir  27243  lgsne0  27246  nosupbnd1lem3  27622  nosupbnd1lem4  27623  nosupbnd1lem5  27624  nosupbnd2  27628  noinfbnd1lem3  27637  noinfbnd1lem4  27638  noinfbnd1lem5  27639  noinfbnd2  27643  sltlpss  27819  sleadd1  27896  sltmul2  28074  istrkgcb  28383  axcontlem2  28892  axcontlem7  28897  axcontlem8  28898  subupgr  29214  clwwlknonex2  30038  frgr3v  30204  pjhthmo  31231  xrge0adddir  32959  dimvalfi  33597  pcmplfinf  33851  probun  34410  satfv1lem  35349  trisegint  36016  btwnconn1lem13  36087  outsideoftr  36117  outsideofeq  36118  linethru  36141  isbasisrelowllem1  37343  atlatmstc  39312  cvlcvr1  39332  hlrelat  39396  intnatN  39401  cvrval5  39409  2at0mat0  39519  llncvrlpln  39552  lplnexllnN  39558  lplncvrlvol  39610  lncvrelatN  39775  lncmp  39777  paddasslem5  39818  pmapjoin  39846  pmapjat1  39847  pclclN  39885  lhprelat3N  40034  cdleme32fvcl  40434  cdlemg1a  40564  cdlemg1cN  40581  cdlemg39  40710  ltrncom  40732  dihmeetALTN  41321  dihlspsnat  41327  mapdrvallem2  41639  sticksstones12  42146  mzpsubst  42736  lzunuz  42756  acongeq  42972  jm2.19  42982  jm2.27  42997  aomclem6  43048  lmhmfgsplit  43075  hbtlem5  43117  nadd2rabtr  43373  iunrelexpuztr  43708  ismnu  44250  3adantll3  45036  ioondisj2  45491  ioondisj1  45492  iccintsng  45521  icccncfext  45885  stoweidlem61  46059  fourierdlem42  46147  fourierdlem73  46177  smflimlem2  46770  domnmsuppn0  48357  lincresunit3  48470  nnolog2flm1  48579  itschlc0xyqsol1  48755  itschlc0xyqsol  48756