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  5821  tfrlem1  6366  phplem4dom  6923  phplem4on  6928  fisseneq  6995  suplub2ti  7067  omp1eomlem  7160  nnnninfeq  7194  nninfisol  7199  exmidontriim  7292  addcmpblnq  7434  mulcmpblnq  7435  ordpipqqs  7441  ltexnqq  7475  enq0tr  7501  addcmpblnq0  7510  mulcmpblnq0  7511  nnnq0lem1  7513  prssnql  7546  prmuloc  7633  prmuloc2  7634  mullocpr  7638  ltexprlemopu  7670  ltexprlemrl  7677  ltexprlemru  7679  addcanprleml  7681  addcanprlemu  7682  ltmprr  7709  archpr  7710  suplocexprlemloc  7788  addcmpblnr  7806  mulcmpblnrlemg  7807  mulcmpblnr  7808  ltsrprg  7814  srpospr  7850  axcaucvglemres  7966  axpre-suploclemres  7968  axpre-suploc  7969  negeu  8217  add20  8501  rimul  8612  apreap  8614  cru  8629  mulge0  8646  mulap0  8681  prodgt0  8879  ltmul12a  8887  ledivdiv  8917  lediv12a  8921  qapne  9713  qreccl  9716  xleaddadd  9962  ixxss12  9981  ioodisj  10068  fznlem  10116  elfz0fzfz0  10201  btwnzge0  10390  seqf1og  10613  mulexpzap  10671  leexp1a  10686  expnbnd  10755  hashennnuni  10871  zfz1iso  10933  seq3coll  10934  resqrexlemga  11188  sqrtsq  11209  abs3lem  11276  cau3lem  11279  minmax  11395  xrmaxiflemval  11415  xrminmax  11430  climcau  11512  summodclem2  11547  fsumrelem  11636  cvgratz  11697  mertenslemi1  11700  mertenslem2  11701  mertensabs  11702  fprodcl2lem  11770  fprodap0  11786  fprodrec  11794  fprodap0f  11801  fprodle  11805  dvdsle  12009  bitsfzo  12119  bezoutlemmain  12165  bezoutlemzz  12169  dfgcd3  12177  dvdsmulgcd  12192  lcmcllem  12235  lcmgcdlem  12245  ncoprmgcdne1b  12257  qredeu  12265  oddpwdclemxy  12337  oddpwdclemdc  12341  pythagtriplem2  12435  pythagtrip  12452  pc2dvds  12499  pcz  12501  ctiunctlemfo  12656  unct  12659  sgrppropd  13056  mndpropd  13081  mhmeql  13124  mhmid  13245  mhmmnd  13246  mulgval  13252  issubg4m  13323  imasabl  13466  gsumfzconst  13471  reldvdsrsrg  13648  dvdsrmul1  13658  unitgrp  13672  neissex  14401  restbasg  14404  tgrest  14405  restopnb  14417  cnptopco  14458  metequiv2  14732  xmettx  14746  metcnpi3  14753  mpomulcn  14802  fsumcncntop  14803  elcncf2  14810  cncfmet  14828  dedekindeulemuub  14853  dedekindeulemlu  14857  dedekindicclemuub  14862  dedekindicclemlu  14866  limccnpcntop  14911  dvmptfsum  14961  reeff1olem  15007  lgsquad3  15325  nninfalllem1  15652  apdiff  15692