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  7308  addcmpblnq  7451  mulcmpblnq  7452  ordpipqqs  7458  ltexnqq  7492  enq0tr  7518  addcmpblnq0  7527  mulcmpblnq0  7528  nnnq0lem1  7530  prssnql  7563  prmuloc  7650  prmuloc2  7651  mullocpr  7655  ltexprlemopu  7687  ltexprlemrl  7694  ltexprlemru  7696  addcanprleml  7698  addcanprlemu  7699  ltmprr  7726  archpr  7727  suplocexprlemloc  7805  addcmpblnr  7823  mulcmpblnrlemg  7824  mulcmpblnr  7825  ltsrprg  7831  srpospr  7867  axcaucvglemres  7983  axpre-suploclemres  7985  axpre-suploc  7986  negeu  8234  add20  8518  rimul  8629  apreap  8631  cru  8646  mulge0  8663  mulap0  8698  prodgt0  8896  ltmul12a  8904  ledivdiv  8934  lediv12a  8938  qapne  9730  qreccl  9733  xleaddadd  9979  ixxss12  9998  ioodisj  10085  fznlem  10133  elfz0fzfz0  10218  btwnzge0  10407  seqf1og  10630  mulexpzap  10688  leexp1a  10703  expnbnd  10772  hashennnuni  10888  zfz1iso  10950  seq3coll  10951  resqrexlemga  11205  sqrtsq  11226  abs3lem  11293  cau3lem  11296  minmax  11412  xrmaxiflemval  11432  xrminmax  11447  climcau  11529  summodclem2  11564  fsumrelem  11653  cvgratz  11714  mertenslemi1  11717  mertenslem2  11718  mertensabs  11719  fprodcl2lem  11787  fprodap0  11803  fprodrec  11811  fprodap0f  11818  fprodle  11822  dvdsle  12026  bitsfzo  12137  bezoutlemmain  12190  bezoutlemzz  12194  dfgcd3  12202  dvdsmulgcd  12217  lcmcllem  12260  lcmgcdlem  12270  ncoprmgcdne1b  12282  qredeu  12290  oddpwdclemxy  12362  oddpwdclemdc  12366  pythagtriplem2  12460  pythagtrip  12477  pc2dvds  12524  pcz  12526  ctiunctlemfo  12681  unct  12684  sgrppropd  13115  mndpropd  13142  mhmeql  13194  mhmid  13321  mhmmnd  13322  mulgval  13328  issubg4m  13399  imasabl  13542  gsumfzconst  13547  reldvdsrsrg  13724  dvdsrmul1  13734  unitgrp  13748  neissex  14485  restbasg  14488  tgrest  14489  restopnb  14501  cnptopco  14542  metequiv2  14816  xmettx  14830  metcnpi3  14837  mpomulcn  14886  fsumcncntop  14887  elcncf2  14894  cncfmet  14912  dedekindeulemuub  14937  dedekindeulemlu  14941  dedekindicclemuub  14946  dedekindicclemlu  14950  limccnpcntop  14995  dvmptfsum  15045  reeff1olem  15091  lgsquad3  15409  nninfalllem1  15739  apdiff  15779