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  8481  add20  8766  rimul  8877  apreap  8879  cru  8894  mulge0  8911  mulap0  8946  prodgt0  9146  ltmul12a  9154  ledivdiv  9184  lediv12a  9188  qapne  9992  qreccl  9995  xleaddadd  10242  ixxss12  10261  ioodisj  10348  fznlem  10398  elfz0fzfz0  10485  btwnzge0  10687  seqf1og  10910  mulexpzap  10968  leexp1a  10983  expnbnd  11053  hashennnuni  11170  zfz1iso  11241  seq3coll  11242  swrdswrdlem  11424  pfxccatin12lem3  11452  resqrexlemga  11737  sqrtsq  11758  abs3lem  11825  cau3lem  11828  minmax  11944  xrmaxiflemval  11964  xrminmax  11979  climcau  12061  summodclem2  12097  fsumrelem  12186  cvgratz  12247  mertenslemi1  12250  mertenslem2  12251  mertensabs  12252  fprodcl2lem  12320  fprodap0  12336  fprodrec  12344  fprodap0f  12351  fprodle  12355  dvdsle  12559  bitsfzo  12670  bezoutlemmain  12723  bezoutlemzz  12727  dfgcd3  12735  dvdsmulgcd  12750  lcmcllem  12793  lcmgcdlem  12803  ncoprmgcdne1b  12815  qredeu  12823  oddpwdclemxy  12895  oddpwdclemdc  12899  pythagtriplem2  12993  pythagtrip  13010  pc2dvds  13057  pcz  13059  ctiunctlemfo  13278  unct  13281  sgrppropd  13680  mndpropd  13705  mhmeql  13751  mhmid  13872  mhmmnd  13873  mulgval  13879  issubg4m  13950  imasabl  14093  gsumfzconst  14098  gfsumz  14113  dvdsrmul1  14351  unitgrp  14365  aprlring  14542  neissex  15160  restbasg  15163  tgrest  15164  restopnb  15176  cnptopco  15217  metequiv2  15491  xmettx  15505  metcnpi3  15512  mpomulcn  15561  fsumcncntop  15562  elcncf2  15569  cncfmet  15587  dedekindeulemuub  15612  dedekindeulemlu  15616  dedekindicclemuub  15621  dedekindicclemlu  15625  limccnpcntop  15670  dvmptfsum  15720  reeff1olem  15766  lgsquad3  16087  clwwlkccatlem  16525  nninfalllem1  16926  nninfnfiinf  16941  apdiff  16972