Theorem simpll3 1233

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 1156	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜒)
2	1	ad2antrr 739	1 ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜒)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  f1prex  7293  poxp3  8170  naddsuc2  8715  ordiso2  9513  iunfictbso  10197  fin1a2lem12  10493  fin1a2lem13  10494  prlem934  11122  ifle  13331  xlesubadd  13397  icoshftf1o  13609  elfzonelfzo  13908  fsuppmapnn0fiub0  14140  swrdcl  14798  repswccat  14942  subcn2  15768  rpdvds  16841  coprmprod  16842  qexpz  17085  ramval  17192  0ram  17204  cshwrepswhash1  17286  mreexexd  17828  gsmsymgreqlem1  19650  pmtrf  19675  odmulg  19776  pgpfi1  19815  lsmcl  21364  lbsextlem3  21444  islindf4  22150  coe1mul2  22594  cramerlem2  23012  cpmadugsumlemF  23200  cayhamlem4  23212  iscnp4  23587  cnpnei  23588  cnconst2  23607  cnpdis  23617  cnhaus  23678  ordthauslem  23707  clsconn  23754  nlly2i  23801  txcn  23951  ordthmeolem  24126  flimrest  24308  isfcf  24359  alexsubALTlem4  24375  ghmcnp  24440  utop2nei  24575  blssps  24749  blss  24750  metcnp3  24865  metcnp  24866  xrsxmet  25135  metdseq0  25180  xrhmeo  25273  cfil3i  25596  caucfil  25610  cfilres  25623  fta1b  26496  mumul  27514  lgsfcl2  27636  lgsdir  27665  lgsne0  27668  nolt02o  28058  nogt01o  28059  nosupbnd1lem3  28073  nosupbnd1lem4  28074  nosupbnd1lem5  28075  nosupbnd2  28079  noinfbnd1lem3  28088  noinfbnd1lem4  28089  noinfbnd1lem5  28090  noinfbnd2  28094  leadds1  28381  ltmuls2  28563  istrkgcb  28924  axbtwnid  29523  axcontlem2  29549  axcontlem4  29551  axcontlem7  29554  axcontlem8  29555  umgr2v2enb1  30113  frgr3v  30882  extwwlkfab  30959  pjhthmo  31910  xrge0adddir  33626  archiabl  33806  dimvalfi  34281  pcmplfinf  34540  probun  35098  cnpconn  36082  satfv1lem  36214  outsideofeq  36988  linethru  37011  weiunso  37347  atlatmstc  40470  cvlcvr1  40490  ishlat3N  40505  hlrelat  40553  intnatN  40558  cvrval5  40566  atcvrlln  40671  llnexatN  40672  2at0mat0  40676  llncvrlpln  40709  lplnexllnN  40715  lplncvrlvol  40767  lncvrelatN  40932  pmapjoin  41003  pmapjat1  41004  pclclN  41042  osumclN  41118  lhprelat3N  41191  cdlemd5  41353  cdleme32fvcl  41591  cdlemg39  41867  ltrncom  41889  dihmeetALTN  42478  dochss  42516  mapdrvallem2  42796  nacsfix  43817  mzpsubst  43853  diophrw  43864  lzunuz  43873  jm2.19  44094  jm2.27  44109  hbtlem5  44224  tfsconcatrn  44438  nadd2rabtr  44480  fzunt  44550  iunrelexpuztr  44813  grumnudlem  45363  rfcnnnub  46147  3adantll2  46152  infleinf  46477  iccintsng  46629  mullimc  46722  mullimcf  46729  limcperiod  46734  cncfshift  46978  cncfperiod  46983  icccncfext  46991  stoweidlem20  47124  stoweidlem61  47165  fourierdlem73  47283  rmsupp0  49574  rmsuppss  49576  itschlc0xyqsol1  49972  itschlc0xyqsol  49973