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  7341  omp1eomlem  7434  nnnninfeq  7468  nninfisol  7473  exmidontriim  7581  addcmpblnq  7734  mulcmpblnq  7735  ordpipqqs  7741  ltexnqq  7775  enq0tr  7801  addcmpblnq0  7810  mulcmpblnq0  7811  nnnq0lem1  7813  prssnql  7846  prmuloc  7933  prmuloc2  7934  mullocpr  7938  ltexprlemopu  7970  ltexprlemrl  7977  ltexprlemru  7979  addcanprleml  7981  addcanprlemu  7982  ltmprr  8009  archpr  8010  suplocexprlemloc  8088  addcmpblnr  8106  mulcmpblnrlemg  8107  mulcmpblnr  8108  ltsrprg  8114  srpospr  8150  axcaucvglemres  8266  axpre-suploclemres  8268  axpre-suploc  8269  negeu  8517  add20  8802  rimul  8914  apreap  8916  cru  8931  mulge0  8948  mulap0  8983  prodgt0  9183  ltmul12a  9191  ledivdiv  9221  lediv12a  9225  qapne  10041  qreccl  10044  xleaddadd  10291  ixxss12  10310  ioodisj  10397  fznlem  10447  elfz0fzfz0  10535  btwnzge0  10737  seqf1og  10960  mulexpzap  11018  leexp1a  11033  expnbnd  11103  hashennnuni  11220  hashf1lem2  11288  zfz1iso  11295  seq3coll  11296  swrdswrdlem  11478  pfxccatin12lem3  11506  resqrexlemga  11791  sqrtsq  11812  abs3lem  11879  cau3lem  11882  minmax  11998  xrmaxiflemval  12018  xrminmax  12033  climcau  12115  summodclem2  12151  fsumrelem  12240  cvgratz  12301  mertenslemi1  12304  mertenslem2  12305  mertensabs  12306  fprodcl2lem  12374  fprodap0  12390  fprodrec  12398  fprodap0f  12405  fprodle  12409  dvdsle  12613  bitsfzo  12724  bezoutlemmain  12777  bezoutlemzz  12781  dfgcd3  12789  dvdsmulgcd  12804  lcmcllem  12847  lcmgcdlem  12857  ncoprmgcdne1b  12869  qredeu  12877  oddpwdclemxy  12949  oddpwdclemdc  12953  pythagtriplem2  13047  pythagtrip  13064  pc2dvds  13111  pcz  13113  ctiunctlemfo  13332  unct  13335  sgrppropd  13730  mndpropd  13755  mhmeql  13801  mhmid  13920  mhmmnd  13921  mulgval  13927  issubg4m  13998  imasabl  14142  gzsumconst  14145  gsumzfi  14160  gsummptfidmadd  14163  dvdsrmul1  14411  unitgrp  14425  aprlring  14602  gsumfsum  14925  issubassa2  15037  neissex  15268  restbasg  15271  tgrest  15272  restopnb  15284  cnptopco  15325  metequiv2  15599  xmettx  15613  metcnpi3  15620  mpomulcn  15669  fsumcncntop  15670  elcncf2  15677  cncfmet  15695  dedekindeulemuub  15720  dedekindeulemlu  15724  dedekindicclemuub  15729  dedekindicclemlu  15733  limccnpcntop  15778  dvmptfsum  15828  reeff1olem  15874  lgsquad3  16215  clwwlkccatlem  16653  nninfalllem1  17063  nninfnfiinf  17078  apdiff  17109