Theorem simplll 533

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  541  f1imass  5853  tfrlem1  6404  phplem4dom  6971  phplem4on  6976  fisseneq  7043  suplub2ti  7115  omp1eomlem  7208  nnnninfeq  7242  nninfisol  7247  exmidontriim  7350  addcmpblnq  7493  mulcmpblnq  7494  ordpipqqs  7500  ltexnqq  7534  enq0tr  7560  addcmpblnq0  7569  mulcmpblnq0  7570  nnnq0lem1  7572  prssnql  7605  prmuloc  7692  prmuloc2  7693  mullocpr  7697  ltexprlemopu  7729  ltexprlemrl  7736  ltexprlemru  7738  addcanprleml  7740  addcanprlemu  7741  ltmprr  7768  archpr  7769  suplocexprlemloc  7847  addcmpblnr  7865  mulcmpblnrlemg  7866  mulcmpblnr  7867  ltsrprg  7873  srpospr  7909  axcaucvglemres  8025  axpre-suploclemres  8027  axpre-suploc  8028  negeu  8276  add20  8560  rimul  8671  apreap  8673  cru  8688  mulge0  8705  mulap0  8740  prodgt0  8938  ltmul12a  8946  ledivdiv  8976  lediv12a  8980  qapne  9773  qreccl  9776  xleaddadd  10022  ixxss12  10041  ioodisj  10128  fznlem  10176  elfz0fzfz0  10261  btwnzge0  10456  seqf1og  10679  mulexpzap  10737  leexp1a  10752  expnbnd  10821  hashennnuni  10937  zfz1iso  10999  seq3coll  11000  swrdswrdlem  11169  resqrexlemga  11384  sqrtsq  11405  abs3lem  11472  cau3lem  11475  minmax  11591  xrmaxiflemval  11611  xrminmax  11626  climcau  11708  summodclem2  11743  fsumrelem  11832  cvgratz  11893  mertenslemi1  11896  mertenslem2  11897  mertensabs  11898  fprodcl2lem  11966  fprodap0  11982  fprodrec  11990  fprodap0f  11997  fprodle  12001  dvdsle  12205  bitsfzo  12316  bezoutlemmain  12369  bezoutlemzz  12373  dfgcd3  12381  dvdsmulgcd  12396  lcmcllem  12439  lcmgcdlem  12449  ncoprmgcdne1b  12461  qredeu  12469  oddpwdclemxy  12541  oddpwdclemdc  12545  pythagtriplem2  12639  pythagtrip  12656  pc2dvds  12703  pcz  12705  ctiunctlemfo  12860  unct  12863  sgrppropd  13295  mndpropd  13322  mhmeql  13374  mhmid  13501  mhmmnd  13502  mulgval  13508  issubg4m  13579  imasabl  13722  gsumfzconst  13727  reldvdsrsrg  13904  dvdsrmul1  13914  unitgrp  13928  neissex  14687  restbasg  14690  tgrest  14691  restopnb  14703  cnptopco  14744  metequiv2  15018  xmettx  15032  metcnpi3  15039  mpomulcn  15088  fsumcncntop  15089  elcncf2  15096  cncfmet  15114  dedekindeulemuub  15139  dedekindeulemlu  15143  dedekindicclemuub  15148  dedekindicclemlu  15152  limccnpcntop  15197  dvmptfsum  15247  reeff1olem  15293  lgsquad3  15611  nninfalllem1  16060  nninfnfiinf  16075  apdiff  16102