Theorem simpll3 1227

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 1150	. 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:  f1prex  7264  poxp3  8125  naddsuc2  8667  ordiso2  9460  iunfictbso  10067  fin1a2lem12  10365  fin1a2lem13  10366  prlem934  10988  ifle  13197  xlesubadd  13263  icoshftf1o  13475  elfzonelfzo  13772  fsuppmapnn0fiub0  14003  swrdcl  14656  repswccat  14796  subcn2  15605  rpdvds  16677  coprmprod  16678  qexpz  16920  ramval  17027  0ram  17039  cshwrepswhash1  17121  mreexexd  17663  gsmsymgreqlem1  19453  pmtrf  19478  odmulg  19579  pgpfi1  19618  lsmcl  21130  lbsextlem3  21210  islindf4  21870  coe1mul2  22312  cramerlem2  22728  cpmadugsumlemF  22916  cayhamlem4  22928  iscnp4  23303  cnpnei  23304  cnconst2  23323  cnpdis  23333  cnhaus  23394  ordthauslem  23423  clsconn  23470  nlly2i  23516  txcn  23666  ordthmeolem  23841  flimrest  24023  isfcf  24074  alexsubALTlem4  24090  ghmcnp  24155  utop2nei  24290  blssps  24464  blss  24465  metcnp3  24580  metcnp  24581  xrsxmet  24850  metdseq0  24895  xrhmeo  24988  cfil3i  25311  caucfil  25325  cfilres  25338  fta1b  26212  mumul  27222  lgsfcl2  27344  lgsdir  27373  lgsne0  27376  nolt02o  27736  nogt01o  27737  nosupbnd1lem3  27751  nosupbnd1lem4  27752  nosupbnd1lem5  27753  nosupbnd2  27757  noinfbnd1lem3  27766  noinfbnd1lem4  27767  noinfbnd1lem5  27768  noinfbnd2  27772  leadds1  28059  ltmuls2  28241  istrkgcb  28602  axbtwnid  29086  axcontlem2  29112  axcontlem4  29114  axcontlem7  29117  axcontlem8  29118  umgr2v2enb1  29673  frgr3v  30423  extwwlkfab  30500  pjhthmo  31451  xrge0adddir  33157  archiabl  33339  dimvalfi  33860  pcmplfinf  34119  probun  34677  cnpconn  35544  satfv1lem  35676  outsideofeq  36444  linethru  36467  weiunso  36790  atlatmstc  39907  cvlcvr1  39927  ishlat3N  39942  hlrelat  39990  intnatN  39995  cvrval5  40003  atcvrlln  40108  llnexatN  40109  2at0mat0  40113  llncvrlpln  40146  lplnexllnN  40152  lplncvrlvol  40204  lncvrelatN  40369  pmapjoin  40440  pmapjat1  40441  pclclN  40479  osumclN  40555  lhprelat3N  40628  cdlemd5  40790  cdleme32fvcl  41028  cdlemg39  41304  ltrncom  41326  dihmeetALTN  41915  dochss  41953  mapdrvallem2  42233  nacsfix  43257  mzpsubst  43293  diophrw  43304  lzunuz  43313  jm2.19  43534  jm2.27  43549  hbtlem5  43669  tfsconcatrn  43883  nadd2rabtr  43925  fzunt  43995  iunrelexpuztr  44259  grumnudlem  44825  rfcnnnub  45580  3adantll2  45585  infleinf  45911  iccintsng  46063  mullimc  46156  mullimcf  46163  limcperiod  46168  cncfshift  46412  cncfperiod  46417  icccncfext  46425  stoweidlem20  46558  stoweidlem61  46599  fourierdlem73  46717  rmsupp0  48954  rmsuppss  48956  itschlc0xyqsol1  49352  itschlc0xyqsol  49353