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

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1088

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 206  df-an 398  df-3an 1090

This theorem is referenced by:  frpomin  6342  f1prex  7282  poxp3  8136  fprlem2  8286  iunfictbso  10109  fin1a2lem13  10407  prlem934  11028  ifle  13176  ixxlb  13346  elfzonelfzo  13734  swrdcl  14595  subcn2  15539  qexpz  16834  mreexexd  17592  initoeu2lem2  17965  issubmnd  18652  frmdup3lem  18747  pmtrf  19323  pgpssslw  19482  lsmmod  19543  reslmhm2b  20665  lsmcl  20694  lbsextlem3  20773  frlmsslsp  21351  islindf4  21393  coe1mul2  21791  coe1fzgsumdlem  21825  evl1gsumdlem  21875  scmate  22012  mdetdiaglem  22100  madurid  22146  cramerlem2  22190  pmatcollpw3lem  22285  iscnp4  22767  cnrest2  22790  ordthauslem  22887  cncmp  22896  clsconn  22934  rnelfmlem  23456  flimrest  23487  isfcf  23538  cnpfcf  23545  alexsubALT  23555  cldsubg  23615  utop2nei  23755  neipcfilu  23801  blssps  23930  blss  23931  stdbdbl  24026  metcnp3  24049  nmoeq0  24253  xrsxmet  24325  metdseq0  24370  addcnlem  24380  xrhmeo  24462  nmhmcn  24636  cfilres  24813  lgsfcl2  26806  lgsdir  26835  lgsne0  26838  nosupbnd1lem3  27213  nosupbnd1lem4  27214  nosupbnd1lem5  27215  nosupbnd2  27219  noinfbnd1lem3  27228  noinfbnd1lem4  27229  noinfbnd1lem5  27230  noinfbnd2  27234  sltlpss  27401  sleadd1  27472  sltmul2  27623  istrkgcb  27707  axcontlem2  28223  axcontlem7  28228  axcontlem8  28229  subupgr  28544  clwwlknonex2  29362  frgr3v  29528  pjhthmo  30555  xrge0adddir  32193  dimvalfi  32687  pcmplfinf  32841  probun  33418  satfv1lem  34353  trisegint  35000  btwnconn1lem13  35071  outsideoftr  35101  outsideofeq  35102  linethru  35125  isbasisrelowllem1  36236  atlatmstc  38189  cvlcvr1  38209  hlrelat  38273  intnatN  38278  cvrval5  38286  2at0mat0  38396  llncvrlpln  38429  lplnexllnN  38435  lplncvrlvol  38487  lncvrelatN  38652  lncmp  38654  paddasslem5  38695  pmapjoin  38723  pmapjat1  38724  pclclN  38762  lhprelat3N  38911  cdleme32fvcl  39311  cdlemg1a  39441  cdlemg1cN  39458  cdlemg39  39587  ltrncom  39609  dihmeetALTN  40198  dihlspsnat  40204  mapdrvallem2  40516  sticksstones12  40974  mzpsubst  41486  lzunuz  41506  acongeq  41722  jm2.19  41732  jm2.27  41747  aomclem6  41801  lmhmfgsplit  41828  hbtlem5  41870  nadd2rabtr  42134  naddsuc2  42143  iunrelexpuztr  42470  ismnu  43020  3adantll3  43726  ioondisj2  44206  ioondisj1  44207  iccintsng  44236  icccncfext  44603  stoweidlem61  44777  fourierdlem42  44865  fourierdlem73  44895  smflimlem2  45488  domnmsuppn0  47045  lincresunit3  47162  nnolog2flm1  47276  itschlc0xyqsol1  47452  itschlc0xyqsol  47453