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  6298  f1prex  7230  poxp3  8092  fprlem2  8243  naddsuc2  8629  iunfictbso  10024  fin1a2lem13  10322  prlem934  10944  ifle  13112  ixxlb  13283  elfzonelfzo  13685  swrdcl  14569  subcn2  15518  qexpz  16829  mreexexd  17571  initoeu2lem2  17939  issubmnd  18686  frmdup3lem  18791  pmtrf  19384  pgpssslw  19543  lsmmod  19604  reslmhm2b  21006  lsmcl  21035  lbsextlem3  21115  frlmsslsp  21751  islindf4  21793  coe1mul2  22211  coe1fzgsumdlem  22247  evl1gsumdlem  22300  scmate  22454  mdetdiaglem  22542  madurid  22588  cramerlem2  22632  pmatcollpw3lem  22727  iscnp4  23207  cnrest2  23230  ordthauslem  23327  cncmp  23336  clsconn  23374  rnelfmlem  23896  flimrest  23927  isfcf  23978  cnpfcf  23985  alexsubALT  23995  cldsubg  24055  utop2nei  24194  neipcfilu  24239  blssps  24368  blss  24369  stdbdbl  24461  metcnp3  24484  nmoeq0  24680  xrsxmet  24754  metdseq0  24799  addcnlem  24809  xrhmeo  24900  nmhmcn  25076  cfilres  25252  lgsfcl2  27270  lgsdir  27299  lgsne0  27302  nosupbnd1lem3  27678  nosupbnd1lem4  27679  nosupbnd1lem5  27680  nosupbnd2  27684  noinfbnd1lem3  27693  noinfbnd1lem4  27694  noinfbnd1lem5  27695  noinfbnd2  27699  ltslpss  27904  leadds1  27985  ltmuls2  28167  bdayfinbndlem1  28463  istrkgcb  28528  axcontlem2  29038  axcontlem7  29043  axcontlem8  29044  subupgr  29360  clwwlknonex2  30184  frgr3v  30350  pjhthmo  31377  xrge0adddir  33100  dimvalfi  33758  pcmplfinf  34018  probun  34576  satfv1lem  35556  trisegint  36222  btwnconn1lem13  36293  outsideoftr  36323  outsideofeq  36324  linethru  36347  isbasisrelowllem1  37556  atlatmstc  39575  cvlcvr1  39595  hlrelat  39658  intnatN  39663  cvrval5  39671  2at0mat0  39781  llncvrlpln  39814  lplnexllnN  39820  lplncvrlvol  39872  lncvrelatN  40037  lncmp  40039  paddasslem5  40080  pmapjoin  40108  pmapjat1  40109  pclclN  40147  lhprelat3N  40296  cdleme32fvcl  40696  cdlemg1a  40826  cdlemg1cN  40843  cdlemg39  40972  ltrncom  40994  dihmeetALTN  41583  dihlspsnat  41589  mapdrvallem2  41901  sticksstones12  42408  mzpsubst  42986  lzunuz  43006  acongeq  43221  jm2.19  43231  jm2.27  43246  aomclem6  43297  lmhmfgsplit  43324  hbtlem5  43366  nadd2rabtr  43622  iunrelexpuztr  43956  ismnu  44498  3adantll3  45283  ioondisj2  45735  ioondisj1  45736  iccintsng  45765  icccncfext  46127  stoweidlem61  46301  fourierdlem42  46389  fourierdlem73  46419  smflimlem2  47012  domnmsuppn0  48611  lincresunit3  48723  nnolog2flm1  48832  itschlc0xyqsol1  49008  itschlc0xyqsol  49009