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  7288  poxp3  8151  fprlem2  8303  naddsuc2  8693  iunfictbso  10120  fin1a2lem13  10417  prlem934  11045  ifle  13251  ixxlb  13422  elfzonelfzo  13827  swrdcl  14715  subcn2  15684  qexpz  16997  mreexexd  17740  initoeu2lem2  18108  issubmnd  18868  frmdup3lem  18976  pmtrf  19583  pgpssslw  19742  lsmmod  19803  reslmhm2b  21239  lsmcl  21268  lbsextlem3  21348  frlmsslsp  22010  islindf4  22052  coe1mul2  22496  coe1fzgsumdlem  22529  evl1gsumdlem  22582  scmate  22733  mdetdiaglem  22821  madurid  22867  cramerlem2  22914  pmatcollpw3lem  23009  iscnp4  23489  cnrest2  23512  ordthauslem  23609  cncmp  23618  clsconn  23656  rnelfmlem  24179  flimrest  24210  isfcf  24261  cnpfcf  24268  alexsubALT  24278  cldsubg  24338  utop2nei  24477  neipcfilu  24522  blssps  24651  blss  24652  stdbdbl  24744  metcnp3  24767  nmoeq0  24963  xrsxmet  25037  metdseq0  25082  addcnlem  25092  xrhmeo  25175  nmhmcn  25349  cfilres  25525  lgsfcl2  27537  lgsdir  27566  lgsne0  27569  nosupbnd1lem3  27944  nosupbnd1lem4  27945  nosupbnd1lem5  27946  nosupbnd2  27950  noinfbnd1lem3  27959  noinfbnd1lem4  27960  noinfbnd1lem5  27961  noinfbnd2  27965  ltslpss  28171  leadds1  28252  ltmuls2  28434  bdayfinbndlem1  28730  istrkgcb  28795  axcontlem2  29408  axcontlem7  29413  axcontlem8  29414  subupgr  29733  clwwlknonex2  30565  frgr3v  30741  pjhthmo  31769  xrge0adddir  33445  dimvalfi  34099  pcmplfinf  34358  probun  34917  satfv1lem  35928  trisegint  36595  btwnconn1lem13  36666  outsideoftr  36696  outsideofeq  36697  linethru  36720  isbasisrelowllem1  38096  atlatmstc  40179  cvlcvr1  40199  hlrelat  40262  intnatN  40267  cvrval5  40275  2at0mat0  40385  llncvrlpln  40418  lplnexllnN  40424  lplncvrlvol  40476  lncvrelatN  40641  lncmp  40643  paddasslem5  40684  pmapjoin  40712  pmapjat1  40713  pclclN  40751  lhprelat3N  40900  cdleme32fvcl  41300  cdlemg1a  41430  cdlemg1cN  41447  cdlemg39  41576  ltrncom  41598  dihmeetALTN  42187  dihlspsnat  42193  mapdrvallem2  42505  sticksstones12  43011  mzpsubst  43580  lzunuz  43600  acongeq  43811  jm2.19  43821  jm2.27  43836  aomclem6  43887  lmhmfgsplit  43914  hbtlem5  43956  nadd2rabtr  44212  iunrelexpuztr  44546  ismnu  45072  3adantll3  45863  ioondisj2  46310  ioondisj1  46311  iccintsng  46340  icccncfext  46702  stoweidlem61  46876  fourierdlem42  46964  fourierdlem73  46994  smflimlem2  47587  domnmsuppn0  49286  lincresunit3  49398  nnolog2flm1  49507  itschlc0xyqsol1  49683  itschlc0xyqsol  49684