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  5775  tfrlem1  6309  phplem4dom  6862  phplem4on  6867  fisseneq  6931  suplub2ti  7000  omp1eomlem  7093  nnnninfeq  7126  nninfisol  7131  exmidontriim  7224  addcmpblnq  7366  mulcmpblnq  7367  ordpipqqs  7373  ltexnqq  7407  enq0tr  7433  addcmpblnq0  7442  mulcmpblnq0  7443  nnnq0lem1  7445  prssnql  7478  prmuloc  7565  prmuloc2  7566  mullocpr  7570  ltexprlemopu  7602  ltexprlemrl  7609  ltexprlemru  7611  addcanprleml  7613  addcanprlemu  7614  ltmprr  7641  archpr  7642  suplocexprlemloc  7720  addcmpblnr  7738  mulcmpblnrlemg  7739  mulcmpblnr  7740  ltsrprg  7746  srpospr  7782  axcaucvglemres  7898  axpre-suploclemres  7900  axpre-suploc  7901  negeu  8148  add20  8431  rimul  8542  apreap  8544  cru  8559  mulge0  8576  mulap0  8611  prodgt0  8809  ltmul12a  8817  ledivdiv  8847  lediv12a  8851  qapne  9639  qreccl  9642  xleaddadd  9887  ixxss12  9906  ioodisj  9993  fznlem  10041  elfz0fzfz0  10126  btwnzge0  10300  mulexpzap  10560  leexp1a  10575  expnbnd  10644  hashennnuni  10759  zfz1iso  10821  seq3coll  10822  resqrexlemga  11032  sqrtsq  11053  abs3lem  11120  cau3lem  11123  minmax  11238  xrmaxiflemval  11258  xrminmax  11273  climcau  11355  summodclem2  11390  fsumrelem  11479  cvgratz  11540  mertenslemi1  11543  mertenslem2  11544  mertensabs  11545  fprodcl2lem  11613  fprodap0  11629  fprodrec  11637  fprodap0f  11644  fprodle  11648  dvdsle  11850  gcdsupex  11958  gcdsupcl  11959  bezoutlemmain  11999  bezoutlemzz  12003  dfgcd3  12011  dvdsmulgcd  12026  lcmcllem  12067  lcmgcdlem  12077  ncoprmgcdne1b  12089  qredeu  12097  oddpwdclemxy  12169  oddpwdclemdc  12173  pythagtriplem2  12266  pythagtrip  12283  pc2dvds  12329  pcz  12331  ctiunctlemfo  12440  unct  12443  mndpropd  12841  mhmeql  12876  mhmid  12979  mhmmnd  12980  mulgval  12986  issubg4m  13053  reldvdsrsrg  13261  dvdsrmul1  13271  unitgrp  13285  neissex  13668  restbasg  13671  tgrest  13672  restopnb  13684  cnptopco  13725  metequiv2  13999  xmettx  14013  metcnpi3  14020  fsumcncntop  14059  elcncf2  14064  cncfmet  14082  dedekindeulemuub  14098  dedekindeulemlu  14102  dedekindicclemuub  14107  dedekindicclemlu  14111  limccnpcntop  14147  reeff1olem  14195  nninfalllem1  14760  apdiff  14799