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 726	1 ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 1089

This theorem is referenced by:  frpomin  6361  f1prex  7304  poxp3  8175  fprlem2  8326  naddsuc2  8739  iunfictbso  10154  fin1a2lem13  10452  prlem934  11073  ifle  13239  ixxlb  13409  elfzonelfzo  13808  swrdcl  14683  subcn2  15631  qexpz  16939  mreexexd  17691  initoeu2lem2  18060  issubmnd  18774  frmdup3lem  18879  pmtrf  19473  pgpssslw  19632  lsmmod  19693  reslmhm2b  21053  lsmcl  21082  lbsextlem3  21162  frlmsslsp  21816  islindf4  21858  coe1mul2  22272  coe1fzgsumdlem  22307  evl1gsumdlem  22360  scmate  22516  mdetdiaglem  22604  madurid  22650  cramerlem2  22694  pmatcollpw3lem  22789  iscnp4  23271  cnrest2  23294  ordthauslem  23391  cncmp  23400  clsconn  23438  rnelfmlem  23960  flimrest  23991  isfcf  24042  cnpfcf  24049  alexsubALT  24059  cldsubg  24119  utop2nei  24259  neipcfilu  24305  blssps  24434  blss  24435  stdbdbl  24530  metcnp3  24553  nmoeq0  24757  xrsxmet  24831  metdseq0  24876  addcnlem  24886  xrhmeo  24977  nmhmcn  25153  cfilres  25330  lgsfcl2  27347  lgsdir  27376  lgsne0  27379  nosupbnd1lem3  27755  nosupbnd1lem4  27756  nosupbnd1lem5  27757  nosupbnd2  27761  noinfbnd1lem3  27770  noinfbnd1lem4  27771  noinfbnd1lem5  27772  noinfbnd2  27776  sltlpss  27945  sleadd1  28022  sltmul2  28197  istrkgcb  28464  axcontlem2  28980  axcontlem7  28985  axcontlem8  28986  subupgr  29304  clwwlknonex2  30128  frgr3v  30294  pjhthmo  31321  xrge0adddir  33023  dimvalfi  33652  pcmplfinf  33860  probun  34421  satfv1lem  35367  trisegint  36029  btwnconn1lem13  36100  outsideoftr  36130  outsideofeq  36131  linethru  36154  isbasisrelowllem1  37356  atlatmstc  39320  cvlcvr1  39340  hlrelat  39404  intnatN  39409  cvrval5  39417  2at0mat0  39527  llncvrlpln  39560  lplnexllnN  39566  lplncvrlvol  39618  lncvrelatN  39783  lncmp  39785  paddasslem5  39826  pmapjoin  39854  pmapjat1  39855  pclclN  39893  lhprelat3N  40042  cdleme32fvcl  40442  cdlemg1a  40572  cdlemg1cN  40589  cdlemg39  40718  ltrncom  40740  dihmeetALTN  41329  dihlspsnat  41335  mapdrvallem2  41647  sticksstones12  42159  mzpsubst  42759  lzunuz  42779  acongeq  42995  jm2.19  43005  jm2.27  43020  aomclem6  43071  lmhmfgsplit  43098  hbtlem5  43140  nadd2rabtr  43397  iunrelexpuztr  43732  ismnu  44280  3adantll3  45047  ioondisj2  45506  ioondisj1  45507  iccintsng  45536  icccncfext  45902  stoweidlem61  46076  fourierdlem42  46164  fourierdlem73  46194  smflimlem2  46787  domnmsuppn0  48285  lincresunit3  48398  nnolog2flm1  48511  itschlc0xyqsol1  48687  itschlc0xyqsol  48688