Theorem simplll 539

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 492	1 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜑)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  simp-4l  547  f1imass  5980  suppcofn  6506  tfrlem1  6579  phplem4dom  7163  phplem4on  7169  fisseneq  7242  suplub2ti  7342  omp1eomlem  7435  nnnninfeq  7469  nninfisol  7474  exmidontriim  7582  addcmpblnq  7735  mulcmpblnq  7736  ordpipqqs  7742  ltexnqq  7776  enq0tr  7802  addcmpblnq0  7811  mulcmpblnq0  7812  nnnq0lem1  7814  prssnql  7847  prmuloc  7934  prmuloc2  7935  mullocpr  7939  ltexprlemopu  7971  ltexprlemrl  7978  ltexprlemru  7980  addcanprleml  7982  addcanprlemu  7983  ltmprr  8010  archpr  8011  suplocexprlemloc  8089  addcmpblnr  8107  mulcmpblnrlemg  8108  mulcmpblnr  8109  ltsrprg  8115  srpospr  8151  axcaucvglemres  8267  axpre-suploclemres  8269  axpre-suploc  8270  negeu  8519  add20  8804  rimul  8916  apreap  8918  cru  8933  mulge0  8950  mulap0  8985  prodgt0  9185  ltmul12a  9193  ledivdiv  9223  lediv12a  9227  qapne  10049  qreccl  10052  irraddap  10057  xleaddadd  10300  ixxss12  10319  ioodisj  10406  fznlem  10456  elfz0fzfz0  10544  btwnzge0  10749  seqf1og  10972  mulexpzap  11030  leexp1a  11045  expnbnd  11115  hashennnuni  11233  hashf1lem2  11301  zfz1iso  11308  seq3coll  11309  swrdswrdlem  11491  pfxccatin12lem3  11519  resqrexlemga  11804  sqrtsq  11825  abs3lem  11893  cau3lem  11896  minmax  12013  xrmaxiflemval  12034  xrminmax  12049  climcau  12131  summodclem2  12167  fsumrelem  12256  cvgratz  12317  mertenslemi1  12320  mertenslem2  12321  mertensabs  12322  fprodcl2lem  12390  fprodap0  12406  fprodrec  12414  fprodap0f  12421  fprodle  12425  dvdsle  12629  bitsfzo  12740  bezoutlemmain  12793  bezoutlemzz  12797  dfgcd3  12805  dvdsmulgcd  12820  lcmcllem  12863  lcmgcdlem  12873  ncoprmgcdne1b  12885  qredeu  12893  pwbdvdseu  12965  nnmaxpwlemparts  12970  pythagtriplem2  13067  pythagtrip  13084  pc2dvds  13131  pcz  13133  ctiunctlemfo  13381  unct  13384  sgrppropd  13779  mndpropd  13804  mhmeql  13850  mhmid  13969  mhmmnd  13970  mulgval  13976  issubg4m  14047  imasabl  14191  gzsumconst  14194  gsumzfi  14209  gsummptfidmadd  14212  dvdsrmul1  14460  unitgrp  14474  aprlring  14651  gsumfsum  14974  issubassa2  15086  neissex  15318  restbasg  15321  tgrest  15322  restopnb  15334  cnptopco  15375  metequiv2  15649  xmettx  15663  metcnpi3  15670  mpomulcn  15719  fsumcncntop  15720  elcncf2  15727  cncfmet  15745  dedekindeulemuub  15770  dedekindeulemlu  15774  dedekindicclemuub  15779  dedekindicclemlu  15783  limccnpcntop  15828  dvmptfsum  15878  reeff1olem  15924  lgsquad3  16325  clwwlkccatlem  16763  nninfalllem1  17173  nninfnfiinf  17188  apdiff  17219