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  5953  suppcofn  6479  tfrlem1  6552  phplem4dom  7129  phplem4on  7135  fisseneq  7208  suplub2ti  7305  omp1eomlem  7398  nnnninfeq  7432  nninfisol  7437  exmidontriim  7545  addcmpblnq  7698  mulcmpblnq  7699  ordpipqqs  7705  ltexnqq  7739  enq0tr  7765  addcmpblnq0  7774  mulcmpblnq0  7775  nnnq0lem1  7777  prssnql  7810  prmuloc  7897  prmuloc2  7898  mullocpr  7902  ltexprlemopu  7934  ltexprlemrl  7941  ltexprlemru  7943  addcanprleml  7945  addcanprlemu  7946  ltmprr  7973  archpr  7974  suplocexprlemloc  8052  addcmpblnr  8070  mulcmpblnrlemg  8071  mulcmpblnr  8072  ltsrprg  8078  srpospr  8114  axcaucvglemres  8230  axpre-suploclemres  8232  axpre-suploc  8233  negeu  8480  add20  8765  rimul  8876  apreap  8878  cru  8893  mulge0  8910  mulap0  8945  prodgt0  9143  ltmul12a  9151  ledivdiv  9181  lediv12a  9185  qapne  9989  qreccl  9992  xleaddadd  10239  ixxss12  10258  ioodisj  10345  fznlem  10395  elfz0fzfz0  10482  btwnzge0  10684  seqf1og  10907  mulexpzap  10965  leexp1a  10980  expnbnd  11050  hashennnuni  11167  zfz1iso  11238  seq3coll  11239  swrdswrdlem  11421  pfxccatin12lem3  11449  resqrexlemga  11733  sqrtsq  11754  abs3lem  11821  cau3lem  11824  minmax  11940  xrmaxiflemval  11960  xrminmax  11975  climcau  12057  summodclem2  12093  fsumrelem  12182  cvgratz  12243  mertenslemi1  12246  mertenslem2  12247  mertensabs  12248  fprodcl2lem  12316  fprodap0  12332  fprodrec  12340  fprodap0f  12347  fprodle  12351  dvdsle  12555  bitsfzo  12666  bezoutlemmain  12719  bezoutlemzz  12723  dfgcd3  12731  dvdsmulgcd  12746  lcmcllem  12789  lcmgcdlem  12799  ncoprmgcdne1b  12811  qredeu  12819  oddpwdclemxy  12891  oddpwdclemdc  12895  pythagtriplem2  12989  pythagtrip  13006  pc2dvds  13053  pcz  13055  ctiunctlemfo  13274  unct  13277  sgrppropd  13710  mndpropd  13737  mhmeql  13789  mhmid  13916  mhmmnd  13917  mulgval  13923  issubg4m  13994  imasabl  14137  gsumfzconst  14142  dvdsrmul1  14332  unitgrp  14346  aprlring  14523  neissex  15142  restbasg  15145  tgrest  15146  restopnb  15158  cnptopco  15199  metequiv2  15473  xmettx  15487  metcnpi3  15494  mpomulcn  15543  fsumcncntop  15544  elcncf2  15551  cncfmet  15569  dedekindeulemuub  15594  dedekindeulemlu  15598  dedekindicclemuub  15603  dedekindicclemlu  15607  limccnpcntop  15652  dvmptfsum  15702  reeff1olem  15748  lgsquad3  16069  clwwlkccatlem  16507  nninfalllem1  16898  nninfnfiinf  16913  apdiff  16944  gfsumz  16981