Theorem simpll3 1214

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 1138	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜒)
2	1	ad2antrr 725	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  7320  poxp3  8191  naddsuc2  8757  ordiso2  9584  iunfictbso  10183  fin1a2lem12  10480  fin1a2lem13  10481  prlem934  11102  ifle  13259  xlesubadd  13325  icoshftf1o  13534  elfzonelfzo  13819  fsuppmapnn0fiub0  14044  swrdcl  14693  repswccat  14834  subcn2  15641  rpdvds  16707  coprmprod  16708  qexpz  16948  ramval  17055  0ram  17067  cshwrepswhash1  17150  mreexexd  17706  gsmsymgreqlem1  19472  pmtrf  19497  odmulg  19598  pgpfi1  19637  lsmcl  21105  lbsextlem3  21185  islindf4  21881  coe1mul2  22293  cramerlem2  22715  cpmadugsumlemF  22903  cayhamlem4  22915  iscnp4  23292  cnpnei  23293  cnconst2  23312  cnpdis  23322  cnhaus  23383  ordthauslem  23412  clsconn  23459  nlly2i  23505  txcn  23655  ordthmeolem  23830  flimrest  24012  isfcf  24063  alexsubALTlem4  24079  ghmcnp  24144  utop2nei  24280  blssps  24455  blss  24456  metcnp3  24574  metcnp  24575  xrsxmet  24850  metdseq0  24895  xrhmeo  24996  cfil3i  25322  caucfil  25336  cfilres  25349  fta1b  26231  mumul  27242  lgsfcl2  27365  lgsdir  27394  lgsne0  27397  nolt02o  27758  nogt01o  27759  nosupbnd1lem3  27773  nosupbnd1lem4  27774  nosupbnd1lem5  27775  nosupbnd2  27779  noinfbnd1lem3  27788  noinfbnd1lem4  27789  noinfbnd1lem5  27790  noinfbnd2  27794  sleadd1  28040  sltmul2  28215  istrkgcb  28482  axbtwnid  28972  axcontlem2  28998  axcontlem4  29000  axcontlem7  29003  axcontlem8  29004  umgr2v2enb1  29562  frgr3v  30307  extwwlkfab  30384  pjhthmo  31334  xrge0adddir  33004  archiabl  33178  dimvalfi  33614  pcmplfinf  33807  probun  34384  cnpconn  35198  satfv1lem  35330  outsideofeq  36094  linethru  36117  weiunso  36432  atlatmstc  39275  cvlcvr1  39295  ishlat3N  39310  hlrelat  39359  intnatN  39364  cvrval5  39372  atcvrlln  39477  llnexatN  39478  2at0mat0  39482  llncvrlpln  39515  lplnexllnN  39521  lplncvrlvol  39573  lncvrelatN  39738  pmapjoin  39809  pmapjat1  39810  pclclN  39848  osumclN  39924  lhprelat3N  39997  cdlemd5  40159  cdleme32fvcl  40397  cdlemg39  40673  ltrncom  40695  dihmeetALTN  41284  dochss  41322  mapdrvallem2  41602  nacsfix  42668  mzpsubst  42704  diophrw  42715  lzunuz  42724  jm2.19  42950  jm2.27  42965  hbtlem5  43085  tfsconcatrn  43304  nadd2rabtr  43346  fzunt  43417  iunrelexpuztr  43681  grumnudlem  44254  rfcnnnub  44936  3adantll2  44941  infleinf  45287  iccintsng  45441  mullimc  45537  mullimcf  45544  limcperiod  45549  cncfshift  45795  cncfperiod  45800  icccncfext  45808  stoweidlem20  45941  stoweidlem61  45982  fourierdlem73  46100  rmsupp0  48093  rmsuppss  48095  itschlc0xyqsol1  48500  itschlc0xyqsol  48501