Theorem simplll 522

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 479	1 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 103

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

This theorem is referenced by:  simp-4l  530  f1imass  5668  tfrlem1  6198  phplem4dom  6749  phplem4on  6754  fisseneq  6813  suplub2ti  6881  omp1eomlem  6972  addcmpblnq  7168  mulcmpblnq  7169  ordpipqqs  7175  ltexnqq  7209  enq0tr  7235  addcmpblnq0  7244  mulcmpblnq0  7245  nnnq0lem1  7247  prssnql  7280  prmuloc  7367  prmuloc2  7368  mullocpr  7372  ltexprlemopu  7404  ltexprlemrl  7411  ltexprlemru  7413  addcanprleml  7415  addcanprlemu  7416  ltmprr  7443  archpr  7444  suplocexprlemloc  7522  addcmpblnr  7540  mulcmpblnrlemg  7541  mulcmpblnr  7542  ltsrprg  7548  srpospr  7584  axcaucvglemres  7700  axpre-suploclemres  7702  axpre-suploc  7703  negeu  7946  add20  8229  rimul  8340  apreap  8342  cru  8357  mulge0  8374  mulap0  8408  prodgt0  8603  ltmul12a  8611  ledivdiv  8641  lediv12a  8645  qapne  9424  qreccl  9427  xleaddadd  9663  ixxss12  9682  ioodisj  9769  fznlem  9814  elfz0fzfz0  9896  btwnzge0  10066  mulexpzap  10326  leexp1a  10341  expnbnd  10408  hashennnuni  10518  zfz1iso  10577  seq3coll  10578  resqrexlemga  10788  sqrtsq  10809  abs3lem  10876  cau3lem  10879  minmax  10994  xrmaxiflemval  11012  xrminmax  11027  climcau  11109  summodclem2  11144  fsumrelem  11233  cvgratz  11294  mertenslemi1  11297  mertenslem2  11298  mertensabs  11299  dvdsle  11531  gcdsupex  11635  gcdsupcl  11636  bezoutlemmain  11675  bezoutlemzz  11679  dfgcd3  11687  dvdsmulgcd  11702  lcmcllem  11737  lcmgcdlem  11747  ncoprmgcdne1b  11759  qredeu  11767  oddpwdclemxy  11836  oddpwdclemdc  11840  ctiunctlemfo  11941  unct  11943  neissex  12323  restbasg  12326  tgrest  12327  restopnb  12339  cnptopco  12380  metequiv2  12654  xmettx  12668  metcnpi3  12675  fsumcncntop  12714  elcncf2  12719  cncfmet  12737  dedekindeulemuub  12753  dedekindeulemlu  12757  dedekindicclemuub  12762  dedekindicclemlu  12766  limccnpcntop  12802  nninfalllemn  13191  nninfalllem1  13192