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  5824  tfrlem1  6375  phplem4dom  6932  phplem4on  6937  fisseneq  7004  suplub2ti  7076  omp1eomlem  7169  nnnninfeq  7203  nninfisol  7208  exmidontriim  7310  addcmpblnq  7453  mulcmpblnq  7454  ordpipqqs  7460  ltexnqq  7494  enq0tr  7520  addcmpblnq0  7529  mulcmpblnq0  7530  nnnq0lem1  7532  prssnql  7565  prmuloc  7652  prmuloc2  7653  mullocpr  7657  ltexprlemopu  7689  ltexprlemrl  7696  ltexprlemru  7698  addcanprleml  7700  addcanprlemu  7701  ltmprr  7728  archpr  7729  suplocexprlemloc  7807  addcmpblnr  7825  mulcmpblnrlemg  7826  mulcmpblnr  7827  ltsrprg  7833  srpospr  7869  axcaucvglemres  7985  axpre-suploclemres  7987  axpre-suploc  7988  negeu  8236  add20  8520  rimul  8631  apreap  8633  cru  8648  mulge0  8665  mulap0  8700  prodgt0  8898  ltmul12a  8906  ledivdiv  8936  lediv12a  8940  qapne  9732  qreccl  9735  xleaddadd  9981  ixxss12  10000  ioodisj  10087  fznlem  10135  elfz0fzfz0  10220  btwnzge0  10409  seqf1og  10632  mulexpzap  10690  leexp1a  10705  expnbnd  10774  hashennnuni  10890  zfz1iso  10952  seq3coll  10953  resqrexlemga  11207  sqrtsq  11228  abs3lem  11295  cau3lem  11298  minmax  11414  xrmaxiflemval  11434  xrminmax  11449  climcau  11531  summodclem2  11566  fsumrelem  11655  cvgratz  11716  mertenslemi1  11719  mertenslem2  11720  mertensabs  11721  fprodcl2lem  11789  fprodap0  11805  fprodrec  11813  fprodap0f  11820  fprodle  11824  dvdsle  12028  bitsfzo  12139  bezoutlemmain  12192  bezoutlemzz  12196  dfgcd3  12204  dvdsmulgcd  12219  lcmcllem  12262  lcmgcdlem  12272  ncoprmgcdne1b  12284  qredeu  12292  oddpwdclemxy  12364  oddpwdclemdc  12368  pythagtriplem2  12462  pythagtrip  12479  pc2dvds  12526  pcz  12528  ctiunctlemfo  12683  unct  12686  sgrppropd  13117  mndpropd  13144  mhmeql  13196  mhmid  13323  mhmmnd  13324  mulgval  13330  issubg4m  13401  imasabl  13544  gsumfzconst  13549  reldvdsrsrg  13726  dvdsrmul1  13736  unitgrp  13750  neissex  14509  restbasg  14512  tgrest  14513  restopnb  14525  cnptopco  14566  metequiv2  14840  xmettx  14854  metcnpi3  14861  mpomulcn  14910  fsumcncntop  14911  elcncf2  14918  cncfmet  14936  dedekindeulemuub  14961  dedekindeulemlu  14965  dedekindicclemuub  14970  dedekindicclemlu  14974  limccnpcntop  15019  dvmptfsum  15069  reeff1olem  15115  lgsquad3  15433  nninfalllem1  15763  nninfnfiinf  15778  apdiff  15805