Theorem simpll2 1232

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  frpomin  6342  f1prex  7289  poxp3  8152  fprlem2  8304  naddsuc2  8694  iunfictbso  10121  fin1a2lem13  10418  prlem934  11046  ifle  13253  ixxlb  13424  elfzonelfzo  13829  swrdcl  14717  subcn2  15686  qexpz  16999  mreexexd  17742  initoeu2lem2  18110  issubmnd  18872  frmdup3lem  18981  pmtrf  19588  pgpssslw  19747  lsmmod  19808  reslmhm2b  21244  lsmcl  21273  lbsextlem3  21353  frlmsslsp  22015  islindf4  22057  coe1mul2  22501  coe1fzgsumdlem  22534  evl1gsumdlem  22587  scmate  22738  mdetdiaglem  22826  madurid  22872  cramerlem2  22919  pmatcollpw3lem  23014  iscnp4  23494  cnrest2  23517  ordthauslem  23614  cncmp  23623  clsconn  23661  rnelfmlem  24184  flimrest  24215  isfcf  24266  cnpfcf  24273  alexsubALT  24283  cldsubg  24343  utop2nei  24482  neipcfilu  24527  blssps  24656  blss  24657  stdbdbl  24749  metcnp3  24772  nmoeq0  24968  xrsxmet  25042  metdseq0  25087  addcnlem  25097  xrhmeo  25180  nmhmcn  25354  cfilres  25530  lgsfcl2  27547  lgsdir  27576  lgsne0  27579  nosupbnd1lem3  27954  nosupbnd1lem4  27955  nosupbnd1lem5  27956  nosupbnd2  27960  noinfbnd1lem3  27969  noinfbnd1lem4  27970  noinfbnd1lem5  27971  noinfbnd2  27975  ltslpss  28181  leadds1  28262  ltmuls2  28444  bdayfinbndlem1  28740  istrkgcb  28805  axcontlem2  29430  axcontlem7  29435  axcontlem8  29436  subupgr  29755  clwwlknonex2  30587  frgr3v  30763  pjhthmo  31791  xrge0adddir  33466  dimvalfi  34120  pcmplfinf  34379  probun  34938  satfv1lem  35949  trisegint  36616  btwnconn1lem13  36687  outsideoftr  36717  outsideofeq  36718  linethru  36741  isbasisrelowllem1  38117  atlatmstc  40200  cvlcvr1  40220  hlrelat  40283  intnatN  40288  cvrval5  40296  2at0mat0  40406  llncvrlpln  40439  lplnexllnN  40445  lplncvrlvol  40497  lncvrelatN  40662  lncmp  40664  paddasslem5  40705  pmapjoin  40733  pmapjat1  40734  pclclN  40772  lhprelat3N  40921  cdleme32fvcl  41321  cdlemg1a  41451  cdlemg1cN  41468  cdlemg39  41597  ltrncom  41619  dihmeetALTN  42208  dihlspsnat  42214  mapdrvallem2  42526  sticksstones12  43032  mzpsubst  43601  lzunuz  43621  acongeq  43832  jm2.19  43842  jm2.27  43857  aomclem6  43908  lmhmfgsplit  43935  hbtlem5  43977  nadd2rabtr  44233  iunrelexpuztr  44567  ismnu  45093  3adantll3  45884  ioondisj2  46331  ioondisj1  46332  iccintsng  46361  icccncfext  46723  stoweidlem61  46897  fourierdlem42  46985  fourierdlem73  47015  smflimlem2  47608  domnmsuppn0  49307  lincresunit3  49419  nnolog2flm1  49528  itschlc0xyqsol1  49704  itschlc0xyqsol  49705