Theorem simplll 535

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  543  f1imass  5946  suppcofn  6465  tfrlem1  6538  phplem4dom  7115  phplem4on  7121  fisseneq  7194  suplub2ti  7291  omp1eomlem  7384  nnnninfeq  7418  nninfisol  7423  exmidontriim  7531  addcmpblnq  7681  mulcmpblnq  7682  ordpipqqs  7688  ltexnqq  7722  enq0tr  7748  addcmpblnq0  7757  mulcmpblnq0  7758  nnnq0lem1  7760  prssnql  7793  prmuloc  7880  prmuloc2  7881  mullocpr  7885  ltexprlemopu  7917  ltexprlemrl  7924  ltexprlemru  7926  addcanprleml  7928  addcanprlemu  7929  ltmprr  7956  archpr  7957  suplocexprlemloc  8035  addcmpblnr  8053  mulcmpblnrlemg  8054  mulcmpblnr  8055  ltsrprg  8061  srpospr  8097  axcaucvglemres  8213  axpre-suploclemres  8215  axpre-suploc  8216  negeu  8463  add20  8747  rimul  8858  apreap  8860  cru  8875  mulge0  8892  mulap0  8927  prodgt0  9125  ltmul12a  9133  ledivdiv  9163  lediv12a  9167  qapne  9970  qreccl  9973  xleaddadd  10219  ixxss12  10238  ioodisj  10325  fznlem  10374  elfz0fzfz0  10459  btwnzge0  10659  seqf1og  10882  mulexpzap  10940  leexp1a  10955  expnbnd  11024  hashennnuni  11140  zfz1iso  11209  seq3coll  11210  swrdswrdlem  11392  pfxccatin12lem3  11420  resqrexlemga  11704  sqrtsq  11725  abs3lem  11792  cau3lem  11795  minmax  11911  xrmaxiflemval  11931  xrminmax  11946  climcau  12028  summodclem2  12064  fsumrelem  12153  cvgratz  12214  mertenslemi1  12217  mertenslem2  12218  mertensabs  12219  fprodcl2lem  12287  fprodap0  12303  fprodrec  12311  fprodap0f  12318  fprodle  12322  dvdsle  12526  bitsfzo  12637  bezoutlemmain  12690  bezoutlemzz  12694  dfgcd3  12702  dvdsmulgcd  12717  lcmcllem  12760  lcmgcdlem  12770  ncoprmgcdne1b  12782  qredeu  12790  oddpwdclemxy  12862  oddpwdclemdc  12866  pythagtriplem2  12960  pythagtrip  12977  pc2dvds  13024  pcz  13026  ctiunctlemfo  13182  unct  13185  sgrppropd  13618  mndpropd  13645  mhmeql  13697  mhmid  13824  mhmmnd  13825  mulgval  13831  issubg4m  13902  imasabl  14045  gsumfzconst  14050  dvdsrmul1  14239  unitgrp  14253  aprlring  14426  neissex  15022  restbasg  15025  tgrest  15026  restopnb  15038  cnptopco  15079  metequiv2  15353  xmettx  15367  metcnpi3  15374  mpomulcn  15423  fsumcncntop  15424  elcncf2  15431  cncfmet  15449  dedekindeulemuub  15474  dedekindeulemlu  15478  dedekindicclemuub  15483  dedekindicclemlu  15487  limccnpcntop  15532  dvmptfsum  15582  reeff1olem  15628  lgsquad3  15949  clwwlkccatlem  16387  nninfalllem1  16778  nninfnfiinf  16793  apdiff  16824  gfsumz  16860