Theorem simplll 505

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 108	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)
2	1	ad2antrr 477	1 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  simp-4l  513  f1imass  5629  tfrlem1  6159  phplem4dom  6709  phplem4on  6714  fisseneq  6773  suplub2ti  6840  omp1eomlem  6931  addcmpblnq  7123  mulcmpblnq  7124  ordpipqqs  7130  ltexnqq  7164  enq0tr  7190  addcmpblnq0  7199  mulcmpblnq0  7200  nnnq0lem1  7202  prssnql  7235  prmuloc  7322  prmuloc2  7323  mullocpr  7327  ltexprlemopu  7359  ltexprlemrl  7366  ltexprlemru  7368  addcanprleml  7370  addcanprlemu  7371  ltmprr  7398  archpr  7399  addcmpblnr  7482  mulcmpblnrlemg  7483  mulcmpblnr  7484  ltsrprg  7490  srpospr  7525  axcaucvglemres  7634  negeu  7876  add20  8155  rimul  8265  apreap  8267  cru  8282  mulge0  8299  mulap0  8328  prodgt0  8520  ltmul12a  8528  ledivdiv  8558  lediv12a  8562  qapne  9333  qreccl  9336  xleaddadd  9563  ixxss12  9582  ioodisj  9669  fznlem  9714  elfz0fzfz0  9796  btwnzge0  9966  mulexpzap  10226  leexp1a  10241  expnbnd  10308  hashennnuni  10418  zfz1iso  10477  seq3coll  10478  resqrexlemga  10687  sqrtsq  10708  abs3lem  10775  cau3lem  10778  minmax  10893  xrmaxiflemval  10911  xrminmax  10926  climcau  11008  summodclem2  11043  fsumrelem  11132  cvgratz  11193  mertenslemi1  11196  mertenslem2  11197  mertensabs  11198  dvdsle  11390  gcdsupex  11494  gcdsupcl  11495  bezoutlemmain  11532  bezoutlemzz  11536  dfgcd3  11544  dvdsmulgcd  11559  lcmcllem  11594  lcmgcdlem  11604  ncoprmgcdne1b  11616  qredeu  11624  oddpwdclemxy  11692  oddpwdclemdc  11696  ctiunctlemfo  11795  unct  11797  neissex  12177  restbasg  12180  tgrest  12181  restopnb  12193  cnptopco  12233  metequiv2  12485  xmettx  12499  metcnpi3  12506  fsumcncntop  12542  elcncf2  12547  cncfmet  12565  limccnpcntop  12600  nninfalllemn  12894  nninfalllem1  12895