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  5983  suppcofn  6510  tfrlem1  6583  phplem4dom  7168  phplem4on  7174  fisseneq  7247  suplub2ti  7348  omp1eomlem  7441  nnnninfeq  7475  nninfisol  7480  exmidontriim  7588  addcmpblnq  7741  mulcmpblnq  7742  ordpipqqs  7748  ltexnqq  7782  enq0tr  7808  addcmpblnq0  7817  mulcmpblnq0  7818  nnnq0lem1  7820  prssnql  7853  prmuloc  7940  prmuloc2  7941  mullocpr  7945  ltexprlemopu  7977  ltexprlemrl  7984  ltexprlemru  7986  addcanprleml  7988  addcanprlemu  7989  ltmprr  8016  archpr  8017  suplocexprlemloc  8095  addcmpblnr  8113  mulcmpblnrlemg  8114  mulcmpblnr  8115  ltsrprg  8121  srpospr  8157  axcaucvglemres  8273  axpre-suploclemres  8275  axpre-suploc  8276  negeu  8525  add20  8810  rimul  8922  apreap  8924  cru  8939  mulge0  8956  mulap0  8991  prodgt0  9191  ltmul12a  9199  ledivdiv  9229  lediv12a  9233  qapne  10056  qreccl  10059  irraddap  10064  xleaddadd  10307  ixxss12  10326  ioodisj  10413  fznlem  10463  elfz0fzfz0  10551  btwnzge0  10757  seqf1og  10980  mulexpzap  11038  leexp1a  11053  expnbnd  11123  hashennnuni  11241  hashf1lem2  11309  zfz1iso  11316  seq3coll  11317  swrdswrdlem  11499  pfxccatin12lem3  11527  resqrexlemga  11812  sqrtsq  11833  abs3lem  11901  cau3lem  11904  minmax  12021  xrmaxiflemval  12042  xrminmax  12057  climcau  12139  summodclem2  12175  fsumrelem  12264  cvgratz  12325  mertenslemi1  12328  mertenslem2  12329  mertensabs  12330  fprodcl2lem  12398  fprodap0  12414  fprodrec  12422  fprodap0f  12429  fprodle  12433  dvdsle  12637  bitsfzo  12748  bezoutlemmain  12801  bezoutlemzz  12805  dfgcd3  12813  dvdsmulgcd  12828  lcmcllem  12871  lcmgcdlem  12881  ncoprmgcdne1b  12893  qredeu  12901  pwbdvdseu  12973  nnmaxpwlemparts  12978  pythagtriplem2  13075  pythagtrip  13092  pc2dvds  13139  pcz  13141  ctiunctlemfo  13389  unct  13392  sgrppropd  13788  mndpropd  13813  mhmeql  13859  mhmid  13978  mhmmnd  13979  mulgval  13985  issubg4m  14056  imasabl  14231  gzsumconst  14234  gsumzfi  14249  gsummptfidmadd  14252  gsummptfidmsplit  14255  dvdsrmul1  14519  unitgrp  14533  aprlring  14710  gsumfsum  15033  issubassa2  15145  neissex  15403  restbasg  15406  tgrest  15407  restopnb  15419  cnptopco  15460  metequiv2  15734  xmettx  15748  metcnpi3  15755  mpomulcn  15804  fsumcncntop  15805  elcncf2  15812  cncfmet  15830  dedekindeulemuub  15855  dedekindeulemlu  15859  dedekindicclemuub  15864  dedekindicclemlu  15868  limccnpcntop  15913  dvmptfsum  15963  reeff1olem  16009  lgsquad3  16420  clwwlkccatlem  16858  nninfalllem1  17269  nninfnfiinf  17284  apdiff  17316