Theorem simplll 533

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  541  f1imass  5907  tfrlem1  6465  phplem4dom  7036  phplem4on  7042  fisseneq  7112  suplub2ti  7184  omp1eomlem  7277  nnnninfeq  7311  nninfisol  7316  exmidontriim  7423  addcmpblnq  7570  mulcmpblnq  7571  ordpipqqs  7577  ltexnqq  7611  enq0tr  7637  addcmpblnq0  7646  mulcmpblnq0  7647  nnnq0lem1  7649  prssnql  7682  prmuloc  7769  prmuloc2  7770  mullocpr  7774  ltexprlemopu  7806  ltexprlemrl  7813  ltexprlemru  7815  addcanprleml  7817  addcanprlemu  7818  ltmprr  7845  archpr  7846  suplocexprlemloc  7924  addcmpblnr  7942  mulcmpblnrlemg  7943  mulcmpblnr  7944  ltsrprg  7950  srpospr  7986  axcaucvglemres  8102  axpre-suploclemres  8104  axpre-suploc  8105  negeu  8353  add20  8637  rimul  8748  apreap  8750  cru  8765  mulge0  8782  mulap0  8817  prodgt0  9015  ltmul12a  9023  ledivdiv  9053  lediv12a  9057  qapne  9851  qreccl  9854  xleaddadd  10100  ixxss12  10119  ioodisj  10206  fznlem  10254  elfz0fzfz0  10339  btwnzge0  10537  seqf1og  10760  mulexpzap  10818  leexp1a  10833  expnbnd  10902  hashennnuni  11018  zfz1iso  11081  seq3coll  11082  swrdswrdlem  11257  pfxccatin12lem3  11285  resqrexlemga  11555  sqrtsq  11576  abs3lem  11643  cau3lem  11646  minmax  11762  xrmaxiflemval  11782  xrminmax  11797  climcau  11879  summodclem2  11914  fsumrelem  12003  cvgratz  12064  mertenslemi1  12067  mertenslem2  12068  mertensabs  12069  fprodcl2lem  12137  fprodap0  12153  fprodrec  12161  fprodap0f  12168  fprodle  12172  dvdsle  12376  bitsfzo  12487  bezoutlemmain  12540  bezoutlemzz  12544  dfgcd3  12552  dvdsmulgcd  12567  lcmcllem  12610  lcmgcdlem  12620  ncoprmgcdne1b  12632  qredeu  12640  oddpwdclemxy  12712  oddpwdclemdc  12716  pythagtriplem2  12810  pythagtrip  12827  pc2dvds  12874  pcz  12876  ctiunctlemfo  13031  unct  13034  sgrppropd  13467  mndpropd  13494  mhmeql  13546  mhmid  13673  mhmmnd  13674  mulgval  13680  issubg4m  13751  imasabl  13894  gsumfzconst  13899  dvdsrmul1  14087  unitgrp  14101  neissex  14860  restbasg  14863  tgrest  14864  restopnb  14876  cnptopco  14917  metequiv2  15191  xmettx  15205  metcnpi3  15212  mpomulcn  15261  fsumcncntop  15262  elcncf2  15269  cncfmet  15287  dedekindeulemuub  15312  dedekindeulemlu  15316  dedekindicclemuub  15321  dedekindicclemlu  15325  limccnpcntop  15370  dvmptfsum  15420  reeff1olem  15466  lgsquad3  15784  clwwlkccatlem  16169  nninfalllem1  16488  nninfnfiinf  16503  apdiff  16530