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  6292  f1prex  7224  poxp3  8086  fprlem2  8237  naddsuc2  8622  iunfictbso  10012  fin1a2lem13  10310  prlem934  10931  ifle  13098  ixxlb  13269  elfzonelfzo  13671  swrdcl  14555  subcn2  15504  qexpz  16815  mreexexd  17556  initoeu2lem2  17924  issubmnd  18671  frmdup3lem  18776  pmtrf  19369  pgpssslw  19528  lsmmod  19589  reslmhm2b  20990  lsmcl  21019  lbsextlem3  21099  frlmsslsp  21735  islindf4  21777  coe1mul2  22184  coe1fzgsumdlem  22219  evl1gsumdlem  22272  scmate  22426  mdetdiaglem  22514  madurid  22560  cramerlem2  22604  pmatcollpw3lem  22699  iscnp4  23179  cnrest2  23202  ordthauslem  23299  cncmp  23308  clsconn  23346  rnelfmlem  23868  flimrest  23899  isfcf  23950  cnpfcf  23957  alexsubALT  23967  cldsubg  24027  utop2nei  24166  neipcfilu  24211  blssps  24340  blss  24341  stdbdbl  24433  metcnp3  24456  nmoeq0  24652  xrsxmet  24726  metdseq0  24771  addcnlem  24781  xrhmeo  24872  nmhmcn  25048  cfilres  25224  lgsfcl2  27242  lgsdir  27271  lgsne0  27274  nosupbnd1lem3  27650  nosupbnd1lem4  27651  nosupbnd1lem5  27652  nosupbnd2  27656  noinfbnd1lem3  27665  noinfbnd1lem4  27666  noinfbnd1lem5  27667  noinfbnd2  27671  sltlpss  27854  sleadd1  27933  sltmul2  28111  istrkgcb  28435  axcontlem2  28945  axcontlem7  28950  axcontlem8  28951  subupgr  29267  clwwlknonex2  30091  frgr3v  30257  pjhthmo  31284  xrge0adddir  33006  dimvalfi  33635  pcmplfinf  33895  probun  34453  satfv1lem  35427  trisegint  36093  btwnconn1lem13  36164  outsideoftr  36194  outsideofeq  36195  linethru  36218  isbasisrelowllem1  37420  atlatmstc  39438  cvlcvr1  39458  hlrelat  39521  intnatN  39526  cvrval5  39534  2at0mat0  39644  llncvrlpln  39677  lplnexllnN  39683  lplncvrlvol  39735  lncvrelatN  39900  lncmp  39902  paddasslem5  39943  pmapjoin  39971  pmapjat1  39972  pclclN  40010  lhprelat3N  40159  cdleme32fvcl  40559  cdlemg1a  40689  cdlemg1cN  40706  cdlemg39  40835  ltrncom  40857  dihmeetALTN  41446  dihlspsnat  41452  mapdrvallem2  41764  sticksstones12  42271  mzpsubst  42865  lzunuz  42885  acongeq  43100  jm2.19  43110  jm2.27  43125  aomclem6  43176  lmhmfgsplit  43203  hbtlem5  43245  nadd2rabtr  43501  iunrelexpuztr  43836  ismnu  44378  3adantll3  45163  ioondisj2  45617  ioondisj1  45618  iccintsng  45647  icccncfext  46009  stoweidlem61  46183  fourierdlem42  46271  fourierdlem73  46301  smflimlem2  46894  domnmsuppn0  48493  lincresunit3  48606  nnolog2flm1  48715  itschlc0xyqsol1  48891  itschlc0xyqsol  48892