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  6584  phplem4dom  7169  phplem4on  7175  fisseneq  7248  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  10055  qreccl  10058  irraddap  10063  xleaddadd  10306  ixxss12  10325  ioodisj  10412  fznlem  10462  elfz0fzfz0  10550  btwnzge0  10756  seqf1og  10979  mulexpzap  11037  leexp1a  11052  expnbnd  11122  hashennnuni  11240  hashf1lem2  11308  zfz1iso  11315  seq3coll  11316  swrdswrdlem  11498  pfxccatin12lem3  11526  resqrexlemga  11811  sqrtsq  11832  abs3lem  11900  cau3lem  11903  minmax  12020  xrmaxiflemval  12041  xrminmax  12056  climcau  12138  summodclem2  12174  fsumrelem  12263  cvgratz  12324  mertenslemi1  12327  mertenslem2  12328  mertensabs  12329  fprodcl2lem  12397  fprodap0  12413  fprodrec  12421  fprodap0f  12428  fprodle  12432  dvdsle  12636  bitsfzo  12747  bezoutlemmain  12800  bezoutlemzz  12804  dfgcd3  12812  dvdsmulgcd  12827  lcmcllem  12870  lcmgcdlem  12880  ncoprmgcdne1b  12892  qredeu  12900  pwbdvdseu  12972  nnmaxpwlemparts  12977  pythagtriplem2  13074  pythagtrip  13091  pc2dvds  13138  pcz  13140  ctiunctlemfo  13388  unct  13391  sgrppropd  13787  mndpropd  13812  mhmeql  13858  mhmid  13977  mhmmnd  13978  mulgval  13984  issubg4m  14055  imasabl  14230  gzsumconst  14233  gsumzfi  14248  gsummptfidmadd  14251  gsummptfidmsplit  14254  dvdsrmul1  14518  unitgrp  14532  aprlring  14709  gsumfsum  15032  issubassa2  15144  neissex  15424  restbasg  15427  tgrest  15428  restopnb  15440  cnptopco  15481  metequiv2  15755  xmettx  15769  metcnpi3  15776  mpomulcn  15825  fsumcncntop  15826  elcncf2  15833  cncfmet  15851  dedekindeulemuub  15876  dedekindeulemlu  15880  dedekindicclemuub  15885  dedekindicclemlu  15889  limccnpcntop  15934  dvmptfsum  15984  reeff1olem  16030  lgsquad3  16441  clwwlkccatlem  16879  nninfalllem1  17290  nninfnfiinf  17305  apdiff  17337