Theorem simplll 535

Description: Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)

Assertion

Ref	Expression
simplll	⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜑)

Proof of Theorem simplll

Step	Hyp	Ref	Expression
1		simpl 109	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)
2	1	ad2antrr 488	1 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is referenced by:  simp-4l  543  f1imass  5915  tfrlem1  6474  phplem4dom  7048  phplem4on  7054  fisseneq  7127  suplub2ti  7200  omp1eomlem  7293  nnnninfeq  7327  nninfisol  7332  exmidontriim  7440  addcmpblnq  7587  mulcmpblnq  7588  ordpipqqs  7594  ltexnqq  7628  enq0tr  7654  addcmpblnq0  7663  mulcmpblnq0  7664  nnnq0lem1  7666  prssnql  7699  prmuloc  7786  prmuloc2  7787  mullocpr  7791  ltexprlemopu  7823  ltexprlemrl  7830  ltexprlemru  7832  addcanprleml  7834  addcanprlemu  7835  ltmprr  7862  archpr  7863  suplocexprlemloc  7941  addcmpblnr  7959  mulcmpblnrlemg  7960  mulcmpblnr  7961  ltsrprg  7967  srpospr  8003  axcaucvglemres  8119  axpre-suploclemres  8121  axpre-suploc  8122  negeu  8370  add20  8654  rimul  8765  apreap  8767  cru  8782  mulge0  8799  mulap0  8834  prodgt0  9032  ltmul12a  9040  ledivdiv  9070  lediv12a  9074  qapne  9873  qreccl  9876  xleaddadd  10122  ixxss12  10141  ioodisj  10228  fznlem  10276  elfz0fzfz0  10361  btwnzge0  10561  seqf1og  10784  mulexpzap  10842  leexp1a  10857  expnbnd  10926  hashennnuni  11042  zfz1iso  11106  seq3coll  11107  swrdswrdlem  11289  pfxccatin12lem3  11317  resqrexlemga  11588  sqrtsq  11609  abs3lem  11676  cau3lem  11679  minmax  11795  xrmaxiflemval  11815  xrminmax  11830  climcau  11912  summodclem2  11948  fsumrelem  12037  cvgratz  12098  mertenslemi1  12101  mertenslem2  12102  mertensabs  12103  fprodcl2lem  12171  fprodap0  12187  fprodrec  12195  fprodap0f  12202  fprodle  12206  dvdsle  12410  bitsfzo  12521  bezoutlemmain  12574  bezoutlemzz  12578  dfgcd3  12586  dvdsmulgcd  12601  lcmcllem  12644  lcmgcdlem  12654  ncoprmgcdne1b  12666  qredeu  12674  oddpwdclemxy  12746  oddpwdclemdc  12750  pythagtriplem2  12844  pythagtrip  12861  pc2dvds  12908  pcz  12910  ctiunctlemfo  13065  unct  13068  sgrppropd  13501  mndpropd  13528  mhmeql  13580  mhmid  13707  mhmmnd  13708  mulgval  13714  issubg4m  13785  imasabl  13928  gsumfzconst  13933  dvdsrmul1  14122  unitgrp  14136  neissex  14895  restbasg  14898  tgrest  14899  restopnb  14911  cnptopco  14952  metequiv2  15226  xmettx  15240  metcnpi3  15247  mpomulcn  15296  fsumcncntop  15297  elcncf2  15304  cncfmet  15322  dedekindeulemuub  15347  dedekindeulemlu  15351  dedekindicclemuub  15356  dedekindicclemlu  15360  limccnpcntop  15405  dvmptfsum  15455  reeff1olem  15501  lgsquad3  15819  clwwlkccatlem  16257  nninfalllem1  16636  nninfnfiinf  16651  apdiff  16678