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  5765  tfrlem1  6299  phplem4dom  6852  phplem4on  6857  fisseneq  6921  suplub2ti  6990  omp1eomlem  7083  nnnninfeq  7116  nninfisol  7121  exmidontriim  7214  addcmpblnq  7341  mulcmpblnq  7342  ordpipqqs  7348  ltexnqq  7382  enq0tr  7408  addcmpblnq0  7417  mulcmpblnq0  7418  nnnq0lem1  7420  prssnql  7453  prmuloc  7540  prmuloc2  7541  mullocpr  7545  ltexprlemopu  7577  ltexprlemrl  7584  ltexprlemru  7586  addcanprleml  7588  addcanprlemu  7589  ltmprr  7616  archpr  7617  suplocexprlemloc  7695  addcmpblnr  7713  mulcmpblnrlemg  7714  mulcmpblnr  7715  ltsrprg  7721  srpospr  7757  axcaucvglemres  7873  axpre-suploclemres  7875  axpre-suploc  7876  negeu  8122  add20  8405  rimul  8516  apreap  8518  cru  8533  mulge0  8550  mulap0  8584  prodgt0  8780  ltmul12a  8788  ledivdiv  8818  lediv12a  8822  qapne  9610  qreccl  9613  xleaddadd  9856  ixxss12  9875  ioodisj  9962  fznlem  10009  elfz0fzfz0  10094  btwnzge0  10268  mulexpzap  10528  leexp1a  10543  expnbnd  10611  hashennnuni  10725  zfz1iso  10787  seq3coll  10788  resqrexlemga  10998  sqrtsq  11019  abs3lem  11086  cau3lem  11089  minmax  11204  xrmaxiflemval  11224  xrminmax  11239  climcau  11321  summodclem2  11356  fsumrelem  11445  cvgratz  11506  mertenslemi1  11509  mertenslem2  11510  mertensabs  11511  fprodcl2lem  11579  fprodap0  11595  fprodrec  11603  fprodap0f  11610  fprodle  11614  dvdsle  11815  gcdsupex  11923  gcdsupcl  11924  bezoutlemmain  11964  bezoutlemzz  11968  dfgcd3  11976  dvdsmulgcd  11991  lcmcllem  12032  lcmgcdlem  12042  ncoprmgcdne1b  12054  qredeu  12062  oddpwdclemxy  12134  oddpwdclemdc  12138  pythagtriplem2  12231  pythagtrip  12248  pc2dvds  12294  pcz  12296  ctiunctlemfo  12405  unct  12408  mndpropd  12705  mhmeql  12736  mhmid  12838  mhmmnd  12839  mulgval  12845  neissex  13216  restbasg  13219  tgrest  13220  restopnb  13232  cnptopco  13273  metequiv2  13547  xmettx  13561  metcnpi3  13568  fsumcncntop  13607  elcncf2  13612  cncfmet  13630  dedekindeulemuub  13646  dedekindeulemlu  13650  dedekindicclemuub  13655  dedekindicclemlu  13659  limccnpcntop  13695  reeff1olem  13743  nninfalllem1  14298  apdiff  14337