Theorem simpll3 1212

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  f1prex  7136  ordiso2  9204  iunfictbso  9801  fin1a2lem12  10098  fin1a2lem13  10099  prlem934  10720  ifle  12860  xlesubadd  12926  icoshftf1o  13135  elfzonelfzo  13417  fsuppmapnn0fiub0  13641  swrdcl  14286  repswccat  14427  subcn2  15232  rpdvds  16293  coprmprod  16294  qexpz  16530  ramval  16637  0ram  16649  cshwrepswhash1  16732  mreexexd  17274  gsumccatOLD  18394  gsmsymgreqlem1  18953  pmtrf  18978  odmulg  19078  pgpfi1  19115  lsmcl  20260  lbsextlem3  20337  islindf4  20955  coe1mul2  21350  cramerlem2  21745  cpmadugsumlemF  21933  cayhamlem4  21945  iscnp4  22322  cnpnei  22323  cnconst2  22342  cnpdis  22352  cnhaus  22413  ordthauslem  22442  clsconn  22489  nlly2i  22535  txcn  22685  ordthmeolem  22860  flimrest  23042  isfcf  23093  alexsubALTlem4  23109  ghmcnp  23174  utop2nei  23310  blssps  23485  blss  23486  metcnp3  23602  metcnp  23603  xrsxmet  23878  metdseq0  23923  xrhmeo  24015  cfil3i  24338  caucfil  24352  cfilres  24365  fta1b  25239  mumul  26235  lgsfcl2  26356  lgsdir  26385  lgsne0  26388  istrkgcb  26721  axbtwnid  27210  axcontlem2  27236  axcontlem4  27238  axcontlem7  27241  axcontlem8  27242  umgr2v2enb1  27796  frgr3v  28540  extwwlkfab  28617  pjhthmo  29565  xrge0adddir  31203  archiabl  31354  dimvalfi  31589  pcmplfinf  31713  probun  32286  cnpconn  33092  satfv1lem  33224  nolt02o  33825  nogt01o  33826  nosupbnd1lem3  33840  nosupbnd1lem4  33841  nosupbnd1lem5  33842  nosupbnd2  33846  noinfbnd1lem3  33855  noinfbnd1lem4  33856  noinfbnd1lem5  33857  noinfbnd2  33861  outsideofeq  34359  linethru  34382  atlatmstc  37260  cvlcvr1  37280  ishlat3N  37295  hlrelat  37343  intnatN  37348  cvrval5  37356  atcvrlln  37461  llnexatN  37462  2at0mat0  37466  llncvrlpln  37499  lplnexllnN  37505  lplncvrlvol  37557  lncvrelatN  37722  pmapjoin  37793  pmapjat1  37794  pclclN  37832  osumclN  37908  lhprelat3N  37981  cdlemd5  38143  cdleme32fvcl  38381  cdlemg39  38657  ltrncom  38679  dihmeetALTN  39268  dochss  39306  mapdrvallem2  39586  nacsfix  40450  mzpsubst  40486  diophrw  40497  lzunuz  40506  jm2.19  40731  jm2.27  40746  hbtlem5  40869  iunrelexpuztr  41216  grumnudlem  41792  rfcnnnub  42468  3adantll2  42475  infleinf  42801  iccintsng  42951  mullimc  43047  mullimcf  43054  limcperiod  43059  cncfshift  43305  cncfperiod  43310  icccncfext  43318  stoweidlem20  43451  stoweidlem61  43492  fourierdlem73  43610  rmsupp0  45592  rmsuppss  45594  itschlc0xyqsol1  46000  itschlc0xyqsol  46001