Theorem simpll2 1212

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 1136	. 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  6363  f1prex  7304  poxp3  8174  fprlem2  8325  naddsuc2  8738  iunfictbso  10152  fin1a2lem13  10450  prlem934  11071  ifle  13236  ixxlb  13406  elfzonelfzo  13805  swrdcl  14680  subcn2  15628  qexpz  16935  mreexexd  17693  initoeu2lem2  18069  issubmnd  18787  frmdup3lem  18892  pmtrf  19488  pgpssslw  19647  lsmmod  19708  reslmhm2b  21071  lsmcl  21100  lbsextlem3  21180  frlmsslsp  21834  islindf4  21876  coe1mul2  22288  coe1fzgsumdlem  22323  evl1gsumdlem  22376  scmate  22532  mdetdiaglem  22620  madurid  22666  cramerlem2  22710  pmatcollpw3lem  22805  iscnp4  23287  cnrest2  23310  ordthauslem  23407  cncmp  23416  clsconn  23454  rnelfmlem  23976  flimrest  24007  isfcf  24058  cnpfcf  24065  alexsubALT  24075  cldsubg  24135  utop2nei  24275  neipcfilu  24321  blssps  24450  blss  24451  stdbdbl  24546  metcnp3  24569  nmoeq0  24773  xrsxmet  24845  metdseq0  24890  addcnlem  24900  xrhmeo  24991  nmhmcn  25167  cfilres  25344  lgsfcl2  27362  lgsdir  27391  lgsne0  27394  nosupbnd1lem3  27770  nosupbnd1lem4  27771  nosupbnd1lem5  27772  nosupbnd2  27776  noinfbnd1lem3  27785  noinfbnd1lem4  27786  noinfbnd1lem5  27787  noinfbnd2  27791  sltlpss  27960  sleadd1  28037  sltmul2  28212  istrkgcb  28479  axcontlem2  28995  axcontlem7  29000  axcontlem8  29001  subupgr  29319  clwwlknonex2  30138  frgr3v  30304  pjhthmo  31331  xrge0adddir  33006  dimvalfi  33629  pcmplfinf  33822  probun  34401  satfv1lem  35347  trisegint  36010  btwnconn1lem13  36081  outsideoftr  36111  outsideofeq  36112  linethru  36135  isbasisrelowllem1  37338  atlatmstc  39301  cvlcvr1  39321  hlrelat  39385  intnatN  39390  cvrval5  39398  2at0mat0  39508  llncvrlpln  39541  lplnexllnN  39547  lplncvrlvol  39599  lncvrelatN  39764  lncmp  39766  paddasslem5  39807  pmapjoin  39835  pmapjat1  39836  pclclN  39874  lhprelat3N  40023  cdleme32fvcl  40423  cdlemg1a  40553  cdlemg1cN  40570  cdlemg39  40699  ltrncom  40721  dihmeetALTN  41310  dihlspsnat  41316  mapdrvallem2  41628  sticksstones12  42140  mzpsubst  42736  lzunuz  42756  acongeq  42972  jm2.19  42982  jm2.27  42997  aomclem6  43048  lmhmfgsplit  43075  hbtlem5  43117  nadd2rabtr  43374  iunrelexpuztr  43709  ismnu  44257  3adantll3  44980  ioondisj2  45446  ioondisj1  45447  iccintsng  45476  icccncfext  45843  stoweidlem61  46017  fourierdlem42  46105  fourierdlem73  46135  smflimlem2  46728  domnmsuppn0  48214  lincresunit3  48327  nnolog2flm1  48440  itschlc0xyqsol1  48616  itschlc0xyqsol  48617