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  7240  poxp3  8102  naddsuc2  8639  ordiso2  9432  iunfictbso  10036  fin1a2lem12  10333  fin1a2lem13  10334  prlem934  10956  ifle  13124  xlesubadd  13190  icoshftf1o  13402  elfzonelfzo  13697  fsuppmapnn0fiub0  13928  swrdcl  14581  repswccat  14721  subcn2  15530  rpdvds  16599  coprmprod  16600  qexpz  16841  ramval  16948  0ram  16960  cshwrepswhash1  17042  mreexexd  17583  gsmsymgreqlem1  19371  pmtrf  19396  odmulg  19497  pgpfi1  19536  lsmcl  21047  lbsextlem3  21127  islindf4  21805  coe1mul2  22223  cramerlem2  22644  cpmadugsumlemF  22832  cayhamlem4  22844  iscnp4  23219  cnpnei  23220  cnconst2  23239  cnpdis  23249  cnhaus  23310  ordthauslem  23339  clsconn  23386  nlly2i  23432  txcn  23582  ordthmeolem  23757  flimrest  23939  isfcf  23990  alexsubALTlem4  24006  ghmcnp  24071  utop2nei  24206  blssps  24380  blss  24381  metcnp3  24496  metcnp  24497  xrsxmet  24766  metdseq0  24811  xrhmeo  24912  cfil3i  25237  caucfil  25251  cfilres  25264  fta1b  26145  mumul  27159  lgsfcl2  27282  lgsdir  27311  lgsne0  27314  nolt02o  27675  nogt01o  27676  nosupbnd1lem3  27690  nosupbnd1lem4  27691  nosupbnd1lem5  27692  nosupbnd2  27696  noinfbnd1lem3  27705  noinfbnd1lem4  27706  noinfbnd1lem5  27707  noinfbnd2  27711  leadds1  27997  ltmuls2  28179  istrkgcb  28540  axbtwnid  29024  axcontlem2  29050  axcontlem4  29052  axcontlem7  29055  axcontlem8  29056  umgr2v2enb1  29612  frgr3v  30362  extwwlkfab  30439  pjhthmo  31389  xrge0adddir  33110  archiabl  33291  dimvalfi  33778  pcmplfinf  34038  probun  34596  cnpconn  35443  satfv1lem  35575  outsideofeq  36343  linethru  36366  weiunso  36679  atlatmstc  39689  cvlcvr1  39709  ishlat3N  39724  hlrelat  39772  intnatN  39777  cvrval5  39785  atcvrlln  39890  llnexatN  39891  2at0mat0  39895  llncvrlpln  39928  lplnexllnN  39934  lplncvrlvol  39986  lncvrelatN  40151  pmapjoin  40222  pmapjat1  40223  pclclN  40261  osumclN  40337  lhprelat3N  40410  cdlemd5  40572  cdleme32fvcl  40810  cdlemg39  41086  ltrncom  41108  dihmeetALTN  41697  dochss  41735  mapdrvallem2  42015  nacsfix  43063  mzpsubst  43099  diophrw  43110  lzunuz  43119  jm2.19  43344  jm2.27  43359  hbtlem5  43479  tfsconcatrn  43693  nadd2rabtr  43735  fzunt  43805  iunrelexpuztr  44069  grumnudlem  44635  rfcnnnub  45390  3adantll2  45395  infleinf  45724  iccintsng  45877  mullimc  45970  mullimcf  45977  limcperiod  45982  cncfshift  46226  cncfperiod  46231  icccncfext  46239  stoweidlem20  46372  stoweidlem61  46413  fourierdlem73  46531  rmsupp0  48722  rmsuppss  48724  itschlc0xyqsol1  49120  itschlc0xyqsol  49121