Theorem simpll3 1216

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)

Assertion

Ref	Expression
simpll3	⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜒)

Proof of Theorem simpll3

Step	Hyp	Ref	Expression
1		simp3 1139	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜒)
2	1	ad2antrr 727	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:  f1prex  7239  poxp3  8100  naddsuc2  8637  ordiso2  9430  iunfictbso  10036  fin1a2lem12  10333  fin1a2lem13  10334  prlem934  10956  ifle  13149  xlesubadd  13215  icoshftf1o  13427  elfzonelfzo  13724  fsuppmapnn0fiub0  13955  swrdcl  14608  repswccat  14748  subcn2  15557  rpdvds  16629  coprmprod  16630  qexpz  16872  ramval  16979  0ram  16991  cshwrepswhash1  17073  mreexexd  17614  gsmsymgreqlem1  19405  pmtrf  19430  odmulg  19531  pgpfi1  19570  lsmcl  21078  lbsextlem3  21158  islindf4  21818  coe1mul2  22234  cramerlem2  22653  cpmadugsumlemF  22841  cayhamlem4  22853  iscnp4  23228  cnpnei  23229  cnconst2  23248  cnpdis  23258  cnhaus  23319  ordthauslem  23348  clsconn  23395  nlly2i  23441  txcn  23591  ordthmeolem  23766  flimrest  23948  isfcf  23999  alexsubALTlem4  24015  ghmcnp  24080  utop2nei  24215  blssps  24389  blss  24390  metcnp3  24505  metcnp  24506  xrsxmet  24775  metdseq0  24820  xrhmeo  24913  cfil3i  25236  caucfil  25250  cfilres  25263  fta1b  26137  mumul  27144  lgsfcl2  27266  lgsdir  27295  lgsne0  27298  nolt02o  27659  nogt01o  27660  nosupbnd1lem3  27674  nosupbnd1lem4  27675  nosupbnd1lem5  27676  nosupbnd2  27680  noinfbnd1lem3  27689  noinfbnd1lem4  27690  noinfbnd1lem5  27691  noinfbnd2  27695  leadds1  27981  ltmuls2  28163  istrkgcb  28524  axbtwnid  29008  axcontlem2  29034  axcontlem4  29036  axcontlem7  29039  axcontlem8  29040  umgr2v2enb1  29595  frgr3v  30345  extwwlkfab  30422  pjhthmo  31373  xrge0adddir  33078  archiabl  33259  dimvalfi  33746  pcmplfinf  34005  probun  34563  cnpconn  35412  satfv1lem  35544  outsideofeq  36312  linethru  36335  weiunso  36648  atlatmstc  39765  cvlcvr1  39785  ishlat3N  39800  hlrelat  39848  intnatN  39853  cvrval5  39861  atcvrlln  39966  llnexatN  39967  2at0mat0  39971  llncvrlpln  40004  lplnexllnN  40010  lplncvrlvol  40062  lncvrelatN  40227  pmapjoin  40298  pmapjat1  40299  pclclN  40337  osumclN  40413  lhprelat3N  40486  cdlemd5  40648  cdleme32fvcl  40886  cdlemg39  41162  ltrncom  41184  dihmeetALTN  41773  dochss  41811  mapdrvallem2  42091  nacsfix  43144  mzpsubst  43180  diophrw  43191  lzunuz  43200  jm2.19  43421  jm2.27  43436  hbtlem5  43556  tfsconcatrn  43770  nadd2rabtr  43812  fzunt  43882  iunrelexpuztr  44146  grumnudlem  44712  rfcnnnub  45467  3adantll2  45472  infleinf  45801  iccintsng  45953  mullimc  46046  mullimcf  46053  limcperiod  46058  cncfshift  46302  cncfperiod  46307  icccncfext  46315  stoweidlem20  46448  stoweidlem61  46489  fourierdlem73  46607  rmsupp0  48844  rmsuppss  48846  itschlc0xyqsol1  49242  itschlc0xyqsol  49243