Theorem simpll3 1211

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084

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 210  df-an 400  df-3an 1086

This theorem is referenced by:  f1prex  7018  ordiso2  8963  wemappo  8997  iunfictbso  9525  fin1a2lem12  9822  fin1a2lem13  9823  prlem934  10444  ifle  12578  xlesubadd  12644  icoshftf1o  12852  elfzonelfzo  13134  fsuppmapnn0fiub0  13356  swrdcl  13998  repswccat  14139  subcn2  14943  rpdvds  15994  coprmprod  15995  qexpz  16227  ramval  16334  0ram  16346  cshwrepswhash1  16428  mreexexd  16911  gsumccatOLD  17997  gsmsymgreqlem1  18550  pmtrf  18575  odmulg  18675  pgpfi1  18712  lsmcl  19848  lbsextlem3  19925  islindf4  20527  coe1mul2  20898  cramerlem2  21293  cpmadugsumlemF  21481  cayhamlem4  21493  iscnp4  21868  cnpnei  21869  cnconst2  21888  cnpdis  21898  cnhaus  21959  ordthauslem  21988  clsconn  22035  nlly2i  22081  txcn  22231  ordthmeolem  22406  flimrest  22588  isfcf  22639  alexsubALTlem4  22655  ghmcnp  22720  utop2nei  22856  blssps  23031  blss  23032  metcnp3  23147  metcnp  23148  xrsxmet  23414  metdseq0  23459  xrhmeo  23551  cfil3i  23873  caucfil  23887  cfilres  23900  fta1b  24770  mumul  25766  lgsfcl2  25887  lgsdir  25916  lgsne0  25919  istrkgcb  26250  axbtwnid  26733  axcontlem2  26759  axcontlem4  26761  axcontlem7  26764  axcontlem8  26765  umgr2v2enb1  27316  frgr3v  28060  extwwlkfab  28137  pjhthmo  29085  xrge0adddir  30726  archiabl  30877  dimvalfi  31090  pcmplfinf  31214  probun  31787  cnpconn  32590  satfv1lem  32722  nolt02o  33312  nosupbnd1lem3  33323  nosupbnd1lem4  33324  nosupbnd1lem5  33325  nosupbnd2  33329  outsideofeq  33704  linethru  33727  atlatmstc  36615  cvlcvr1  36635  ishlat3N  36650  hlrelat  36698  intnatN  36703  cvrval5  36711  atcvrlln  36816  llnexatN  36817  2at0mat0  36821  llncvrlpln  36854  lplnexllnN  36860  lplncvrlvol  36912  lncvrelatN  37077  pmapjoin  37148  pmapjat1  37149  pclclN  37187  osumclN  37263  lhprelat3N  37336  cdlemd5  37498  cdleme32fvcl  37736  cdlemg39  38012  ltrncom  38034  dihmeetALTN  38623  dochss  38661  mapdrvallem2  38941  nacsfix  39653  mzpsubst  39689  diophrw  39700  lzunuz  39709  jm2.19  39934  jm2.27  39949  hbtlem5  40072  iunrelexpuztr  40420  grumnudlem  40993  rfcnnnub  41665  3adantll2  41672  infleinf  42004  iccintsng  42160  mullimc  42258  mullimcf  42265  limcperiod  42270  cncfshift  42516  cncfperiod  42521  icccncfext  42529  stoweidlem20  42662  stoweidlem61  42703  fourierdlem73  42821  rmsupp0  44770  rmsuppss  44772  itschlc0xyqsol1  45180  itschlc0xyqsol  45181