Theorem simplll 535

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  543  f1imass  5925  suppcofn  6444  tfrlem1  6517  phplem4dom  7091  phplem4on  7097  fisseneq  7170  suplub2ti  7243  omp1eomlem  7336  nnnninfeq  7370  nninfisol  7375  exmidontriim  7483  addcmpblnq  7630  mulcmpblnq  7631  ordpipqqs  7637  ltexnqq  7671  enq0tr  7697  addcmpblnq0  7706  mulcmpblnq0  7707  nnnq0lem1  7709  prssnql  7742  prmuloc  7829  prmuloc2  7830  mullocpr  7834  ltexprlemopu  7866  ltexprlemrl  7873  ltexprlemru  7875  addcanprleml  7877  addcanprlemu  7878  ltmprr  7905  archpr  7906  suplocexprlemloc  7984  addcmpblnr  8002  mulcmpblnrlemg  8003  mulcmpblnr  8004  ltsrprg  8010  srpospr  8046  axcaucvglemres  8162  axpre-suploclemres  8164  axpre-suploc  8165  negeu  8413  add20  8697  rimul  8808  apreap  8810  cru  8825  mulge0  8842  mulap0  8877  prodgt0  9075  ltmul12a  9083  ledivdiv  9113  lediv12a  9117  qapne  9916  qreccl  9919  xleaddadd  10165  ixxss12  10184  ioodisj  10271  fznlem  10319  elfz0fzfz0  10404  btwnzge0  10604  seqf1og  10827  mulexpzap  10885  leexp1a  10900  expnbnd  10969  hashennnuni  11085  zfz1iso  11149  seq3coll  11150  swrdswrdlem  11332  pfxccatin12lem3  11360  resqrexlemga  11644  sqrtsq  11665  abs3lem  11732  cau3lem  11735  minmax  11851  xrmaxiflemval  11871  xrminmax  11886  climcau  11968  summodclem2  12004  fsumrelem  12093  cvgratz  12154  mertenslemi1  12157  mertenslem2  12158  mertensabs  12159  fprodcl2lem  12227  fprodap0  12243  fprodrec  12251  fprodap0f  12258  fprodle  12262  dvdsle  12466  bitsfzo  12577  bezoutlemmain  12630  bezoutlemzz  12634  dfgcd3  12642  dvdsmulgcd  12657  lcmcllem  12700  lcmgcdlem  12710  ncoprmgcdne1b  12722  qredeu  12730  oddpwdclemxy  12802  oddpwdclemdc  12806  pythagtriplem2  12900  pythagtrip  12917  pc2dvds  12964  pcz  12966  ctiunctlemfo  13121  unct  13124  sgrppropd  13557  mndpropd  13584  mhmeql  13636  mhmid  13763  mhmmnd  13764  mulgval  13770  issubg4m  13841  imasabl  13984  gsumfzconst  13989  dvdsrmul1  14178  unitgrp  14192  neissex  14956  restbasg  14959  tgrest  14960  restopnb  14972  cnptopco  15013  metequiv2  15287  xmettx  15301  metcnpi3  15308  mpomulcn  15357  fsumcncntop  15358  elcncf2  15365  cncfmet  15383  dedekindeulemuub  15408  dedekindeulemlu  15412  dedekindicclemuub  15417  dedekindicclemlu  15421  limccnpcntop  15466  dvmptfsum  15516  reeff1olem  15562  lgsquad3  15883  clwwlkccatlem  16321  nninfalllem1  16714  nninfnfiinf  16729  apdiff  16760