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  5770  tfrlem1  6304  phplem4dom  6857  phplem4on  6862  fisseneq  6926  suplub2ti  6995  omp1eomlem  7088  nnnninfeq  7121  nninfisol  7126  exmidontriim  7219  addcmpblnq  7361  mulcmpblnq  7362  ordpipqqs  7368  ltexnqq  7402  enq0tr  7428  addcmpblnq0  7437  mulcmpblnq0  7438  nnnq0lem1  7440  prssnql  7473  prmuloc  7560  prmuloc2  7561  mullocpr  7565  ltexprlemopu  7597  ltexprlemrl  7604  ltexprlemru  7606  addcanprleml  7608  addcanprlemu  7609  ltmprr  7636  archpr  7637  suplocexprlemloc  7715  addcmpblnr  7733  mulcmpblnrlemg  7734  mulcmpblnr  7735  ltsrprg  7741  srpospr  7777  axcaucvglemres  7893  axpre-suploclemres  7895  axpre-suploc  7896  negeu  8142  add20  8425  rimul  8536  apreap  8538  cru  8553  mulge0  8570  mulap0  8605  prodgt0  8803  ltmul12a  8811  ledivdiv  8841  lediv12a  8845  qapne  9633  qreccl  9636  xleaddadd  9881  ixxss12  9900  ioodisj  9987  fznlem  10034  elfz0fzfz0  10119  btwnzge0  10293  mulexpzap  10553  leexp1a  10568  expnbnd  10636  hashennnuni  10750  zfz1iso  10812  seq3coll  10813  resqrexlemga  11023  sqrtsq  11044  abs3lem  11111  cau3lem  11114  minmax  11229  xrmaxiflemval  11249  xrminmax  11264  climcau  11346  summodclem2  11381  fsumrelem  11470  cvgratz  11531  mertenslemi1  11534  mertenslem2  11535  mertensabs  11536  fprodcl2lem  11604  fprodap0  11620  fprodrec  11628  fprodap0f  11635  fprodle  11639  dvdsle  11840  gcdsupex  11948  gcdsupcl  11949  bezoutlemmain  11989  bezoutlemzz  11993  dfgcd3  12001  dvdsmulgcd  12016  lcmcllem  12057  lcmgcdlem  12067  ncoprmgcdne1b  12079  qredeu  12087  oddpwdclemxy  12159  oddpwdclemdc  12163  pythagtriplem2  12256  pythagtrip  12273  pc2dvds  12319  pcz  12321  ctiunctlemfo  12430  unct  12433  mndpropd  12771  mhmeql  12804  mhmid  12907  mhmmnd  12908  mulgval  12914  issubg4m  12979  reldvdsrsrg  13160  dvdsrmul1  13170  unitgrp  13184  neissex  13447  restbasg  13450  tgrest  13451  restopnb  13463  cnptopco  13504  metequiv2  13778  xmettx  13792  metcnpi3  13799  fsumcncntop  13838  elcncf2  13843  cncfmet  13861  dedekindeulemuub  13877  dedekindeulemlu  13881  dedekindicclemuub  13886  dedekindicclemlu  13890  limccnpcntop  13926  reeff1olem  13974  nninfalllem1  14528  apdiff  14567