Theorem simpll2 1226

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 1149	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜓)
2	1	ad2antrr 736	1 ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  frpomin  6323  f1prex  7264  poxp3  8125  fprlem2  8277  naddsuc2  8667  iunfictbso  10067  fin1a2lem13  10366  prlem934  10988  ifle  13197  ixxlb  13368  elfzonelfzo  13772  swrdcl  14656  subcn2  15605  qexpz  16920  mreexexd  17663  initoeu2lem2  18031  issubmnd  18778  frmdup3lem  18883  pmtrf  19478  pgpssslw  19637  lsmmod  19698  reslmhm2b  21101  lsmcl  21130  lbsextlem3  21210  frlmsslsp  21828  islindf4  21870  coe1mul2  22312  coe1fzgsumdlem  22346  evl1gsumdlem  22399  scmate  22550  mdetdiaglem  22638  madurid  22684  cramerlem2  22728  pmatcollpw3lem  22823  iscnp4  23303  cnrest2  23326  ordthauslem  23423  cncmp  23432  clsconn  23470  rnelfmlem  23992  flimrest  24023  isfcf  24074  cnpfcf  24081  alexsubALT  24091  cldsubg  24151  utop2nei  24290  neipcfilu  24335  blssps  24464  blss  24465  stdbdbl  24557  metcnp3  24580  nmoeq0  24776  xrsxmet  24850  metdseq0  24895  addcnlem  24905  xrhmeo  24988  nmhmcn  25162  cfilres  25338  lgsfcl2  27344  lgsdir  27373  lgsne0  27376  nosupbnd1lem3  27751  nosupbnd1lem4  27752  nosupbnd1lem5  27753  nosupbnd2  27757  noinfbnd1lem3  27766  noinfbnd1lem4  27767  noinfbnd1lem5  27768  noinfbnd2  27772  ltslpss  27978  leadds1  28059  ltmuls2  28241  bdayfinbndlem1  28537  istrkgcb  28602  axcontlem2  29112  axcontlem7  29117  axcontlem8  29118  subupgr  29434  clwwlknonex2  30257  frgr3v  30423  pjhthmo  31451  xrge0adddir  33157  dimvalfi  33860  pcmplfinf  34119  probun  34677  satfv1lem  35676  trisegint  36342  btwnconn1lem13  36413  outsideoftr  36443  outsideofeq  36444  linethru  36467  isbasisrelowllem1  37813  atlatmstc  39907  cvlcvr1  39927  hlrelat  39990  intnatN  39995  cvrval5  40003  2at0mat0  40113  llncvrlpln  40146  lplnexllnN  40152  lplncvrlvol  40204  lncvrelatN  40369  lncmp  40371  paddasslem5  40412  pmapjoin  40440  pmapjat1  40441  pclclN  40479  lhprelat3N  40628  cdleme32fvcl  41028  cdlemg1a  41158  cdlemg1cN  41175  cdlemg39  41304  ltrncom  41326  dihmeetALTN  41915  dihlspsnat  41921  mapdrvallem2  42233  sticksstones12  42739  mzpsubst  43293  lzunuz  43313  acongeq  43524  jm2.19  43534  jm2.27  43549  aomclem6  43600  lmhmfgsplit  43627  hbtlem5  43669  nadd2rabtr  43925  iunrelexpuztr  44259  ismnu  44801  3adantll3  45586  ioondisj2  46033  ioondisj1  46034  iccintsng  46063  icccncfext  46425  stoweidlem61  46599  fourierdlem42  46687  fourierdlem73  46717  smflimlem2  47310  domnmsuppn0  48955  lincresunit3  49067  nnolog2flm1  49176  itschlc0xyqsol1  49352  itschlc0xyqsol  49353