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  5891  tfrlem1  6444  phplem4dom  7011  phplem4on  7017  fisseneq  7084  suplub2ti  7156  omp1eomlem  7249  nnnninfeq  7283  nninfisol  7288  exmidontriim  7395  addcmpblnq  7542  mulcmpblnq  7543  ordpipqqs  7549  ltexnqq  7583  enq0tr  7609  addcmpblnq0  7618  mulcmpblnq0  7619  nnnq0lem1  7621  prssnql  7654  prmuloc  7741  prmuloc2  7742  mullocpr  7746  ltexprlemopu  7778  ltexprlemrl  7785  ltexprlemru  7787  addcanprleml  7789  addcanprlemu  7790  ltmprr  7817  archpr  7818  suplocexprlemloc  7896  addcmpblnr  7914  mulcmpblnrlemg  7915  mulcmpblnr  7916  ltsrprg  7922  srpospr  7958  axcaucvglemres  8074  axpre-suploclemres  8076  axpre-suploc  8077  negeu  8325  add20  8609  rimul  8720  apreap  8722  cru  8737  mulge0  8754  mulap0  8789  prodgt0  8987  ltmul12a  8995  ledivdiv  9025  lediv12a  9029  qapne  9822  qreccl  9825  xleaddadd  10071  ixxss12  10090  ioodisj  10177  fznlem  10225  elfz0fzfz0  10310  btwnzge0  10507  seqf1og  10730  mulexpzap  10788  leexp1a  10803  expnbnd  10872  hashennnuni  10988  zfz1iso  11050  seq3coll  11051  swrdswrdlem  11222  pfxccatin12lem3  11250  resqrexlemga  11520  sqrtsq  11541  abs3lem  11608  cau3lem  11611  minmax  11727  xrmaxiflemval  11747  xrminmax  11762  climcau  11844  summodclem2  11879  fsumrelem  11968  cvgratz  12029  mertenslemi1  12032  mertenslem2  12033  mertensabs  12034  fprodcl2lem  12102  fprodap0  12118  fprodrec  12126  fprodap0f  12133  fprodle  12137  dvdsle  12341  bitsfzo  12452  bezoutlemmain  12505  bezoutlemzz  12509  dfgcd3  12517  dvdsmulgcd  12532  lcmcllem  12575  lcmgcdlem  12585  ncoprmgcdne1b  12597  qredeu  12605  oddpwdclemxy  12677  oddpwdclemdc  12681  pythagtriplem2  12775  pythagtrip  12792  pc2dvds  12839  pcz  12841  ctiunctlemfo  12996  unct  12999  sgrppropd  13432  mndpropd  13459  mhmeql  13511  mhmid  13638  mhmmnd  13639  mulgval  13645  issubg4m  13716  imasabl  13859  gsumfzconst  13864  reldvdsrsrg  14041  dvdsrmul1  14051  unitgrp  14065  neissex  14824  restbasg  14827  tgrest  14828  restopnb  14840  cnptopco  14881  metequiv2  15155  xmettx  15169  metcnpi3  15176  mpomulcn  15225  fsumcncntop  15226  elcncf2  15233  cncfmet  15251  dedekindeulemuub  15276  dedekindeulemlu  15280  dedekindicclemuub  15285  dedekindicclemlu  15289  limccnpcntop  15334  dvmptfsum  15384  reeff1olem  15430  lgsquad3  15748  nninfalllem1  16305  nninfnfiinf  16320  apdiff  16347