Theorem simpll3 1213

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 1137	. 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:  f1prex  7303  poxp3  8173  naddsuc2  8737  ordiso2  9552  iunfictbso  10151  fin1a2lem12  10448  fin1a2lem13  10449  prlem934  11070  ifle  13235  xlesubadd  13301  icoshftf1o  13510  elfzonelfzo  13804  fsuppmapnn0fiub0  14030  swrdcl  14679  repswccat  14820  subcn2  15627  rpdvds  16693  coprmprod  16694  qexpz  16934  ramval  17041  0ram  17053  cshwrepswhash1  17136  mreexexd  17692  gsmsymgreqlem1  19462  pmtrf  19487  odmulg  19588  pgpfi1  19627  lsmcl  21099  lbsextlem3  21179  islindf4  21875  coe1mul2  22287  cramerlem2  22709  cpmadugsumlemF  22897  cayhamlem4  22909  iscnp4  23286  cnpnei  23287  cnconst2  23306  cnpdis  23316  cnhaus  23377  ordthauslem  23406  clsconn  23453  nlly2i  23499  txcn  23649  ordthmeolem  23824  flimrest  24006  isfcf  24057  alexsubALTlem4  24073  ghmcnp  24138  utop2nei  24274  blssps  24449  blss  24450  metcnp3  24568  metcnp  24569  xrsxmet  24844  metdseq0  24889  xrhmeo  24990  cfil3i  25316  caucfil  25330  cfilres  25343  fta1b  26225  mumul  27238  lgsfcl2  27361  lgsdir  27390  lgsne0  27393  nolt02o  27754  nogt01o  27755  nosupbnd1lem3  27769  nosupbnd1lem4  27770  nosupbnd1lem5  27771  nosupbnd2  27775  noinfbnd1lem3  27784  noinfbnd1lem4  27785  noinfbnd1lem5  27786  noinfbnd2  27790  sleadd1  28036  sltmul2  28211  istrkgcb  28478  axbtwnid  28968  axcontlem2  28994  axcontlem4  28996  axcontlem7  28999  axcontlem8  29000  umgr2v2enb1  29558  frgr3v  30303  extwwlkfab  30380  pjhthmo  31330  xrge0adddir  33005  archiabl  33187  dimvalfi  33628  pcmplfinf  33821  probun  34400  cnpconn  35214  satfv1lem  35346  outsideofeq  36111  linethru  36134  weiunso  36448  atlatmstc  39300  cvlcvr1  39320  ishlat3N  39335  hlrelat  39384  intnatN  39389  cvrval5  39397  atcvrlln  39502  llnexatN  39503  2at0mat0  39507  llncvrlpln  39540  lplnexllnN  39546  lplncvrlvol  39598  lncvrelatN  39763  pmapjoin  39834  pmapjat1  39835  pclclN  39873  osumclN  39949  lhprelat3N  40022  cdlemd5  40184  cdleme32fvcl  40422  cdlemg39  40698  ltrncom  40720  dihmeetALTN  41309  dochss  41347  mapdrvallem2  41627  nacsfix  42699  mzpsubst  42735  diophrw  42746  lzunuz  42755  jm2.19  42981  jm2.27  42996  hbtlem5  43116  tfsconcatrn  43331  nadd2rabtr  43373  fzunt  43444  iunrelexpuztr  43708  grumnudlem  44280  rfcnnnub  44973  3adantll2  44978  infleinf  45321  iccintsng  45475  mullimc  45571  mullimcf  45578  limcperiod  45583  cncfshift  45829  cncfperiod  45834  icccncfext  45842  stoweidlem20  45975  stoweidlem61  46016  fourierdlem73  46134  rmsupp0  48212  rmsuppss  48214  itschlc0xyqsol1  48615  itschlc0xyqsol  48616