Theorem simplll 499

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

Syntax hints:   → wi 4   ∧ wa 102

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

This theorem is referenced by:  simp-4l  507  f1imass  5434  tfrlem1  5946  phplem4dom  6348  phplem4on  6353  suplub2ti  6414  addcmpblnq  6557  mulcmpblnq  6558  ordpipqqs  6564  ltexnqq  6598  enq0tr  6624  addcmpblnq0  6633  mulcmpblnq0  6634  nnnq0lem1  6636  prssnql  6669  prmuloc  6756  prmuloc2  6757  mullocpr  6761  ltexprlemopu  6793  ltexprlemrl  6800  ltexprlemru  6802  addcanprleml  6804  addcanprlemu  6805  ltmprr  6832  archpr  6833  addcmpblnr  6916  mulcmpblnrlemg  6917  mulcmpblnr  6918  ltsrprg  6924  srpospr  6959  axcaucvglemres  7065  negeu  7299  add20  7578  rimul  7685  apreap  7687  cru  7702  mulge0  7719  mulap0  7744  prodgt0  7930  ltmul12a  7938  ledivdiv  7968  lediv12a  7972  qapne  8724  qreccl  8727  ixxss12  8929  ioodisj  9015  fznlem  9060  elfz0fzfz0  9137  btwnzge0  9302  mulexpzap  9516  leexp1a  9531  expnbnd  9596  resqrexlemga  9909  sqrtsq  9930  abs3lem  9997  cau3lem  10000  minmax  10112  climcau  10184  dvdsle  10244  gcdsupex  10349  gcdsupcl  10350  bezoutlemmain  10387  bezoutlemzz  10391  dfgcd3  10399  dvdsmulgcd  10414  lcmcllem  10449  lcmgcdlem  10459  ncoprmgcdne1b  10471  qredeu  10479  oddpwdclemxy  10547  oddpwdclemdc  10551