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  5910  tfrlem1  6469  phplem4dom  7043  phplem4on  7049  fisseneq  7121  suplub2ti  7194  omp1eomlem  7287  nnnninfeq  7321  nninfisol  7326  exmidontriim  7433  addcmpblnq  7580  mulcmpblnq  7581  ordpipqqs  7587  ltexnqq  7621  enq0tr  7647  addcmpblnq0  7656  mulcmpblnq0  7657  nnnq0lem1  7659  prssnql  7692  prmuloc  7779  prmuloc2  7780  mullocpr  7784  ltexprlemopu  7816  ltexprlemrl  7823  ltexprlemru  7825  addcanprleml  7827  addcanprlemu  7828  ltmprr  7855  archpr  7856  suplocexprlemloc  7934  addcmpblnr  7952  mulcmpblnrlemg  7953  mulcmpblnr  7954  ltsrprg  7960  srpospr  7996  axcaucvglemres  8112  axpre-suploclemres  8114  axpre-suploc  8115  negeu  8363  add20  8647  rimul  8758  apreap  8760  cru  8775  mulge0  8792  mulap0  8827  prodgt0  9025  ltmul12a  9033  ledivdiv  9063  lediv12a  9067  qapne  9866  qreccl  9869  xleaddadd  10115  ixxss12  10134  ioodisj  10221  fznlem  10269  elfz0fzfz0  10354  btwnzge0  10553  seqf1og  10776  mulexpzap  10834  leexp1a  10849  expnbnd  10918  hashennnuni  11034  zfz1iso  11098  seq3coll  11099  swrdswrdlem  11278  pfxccatin12lem3  11306  resqrexlemga  11577  sqrtsq  11598  abs3lem  11665  cau3lem  11668  minmax  11784  xrmaxiflemval  11804  xrminmax  11819  climcau  11901  summodclem2  11936  fsumrelem  12025  cvgratz  12086  mertenslemi1  12089  mertenslem2  12090  mertensabs  12091  fprodcl2lem  12159  fprodap0  12175  fprodrec  12183  fprodap0f  12190  fprodle  12194  dvdsle  12398  bitsfzo  12509  bezoutlemmain  12562  bezoutlemzz  12566  dfgcd3  12574  dvdsmulgcd  12589  lcmcllem  12632  lcmgcdlem  12642  ncoprmgcdne1b  12654  qredeu  12662  oddpwdclemxy  12734  oddpwdclemdc  12738  pythagtriplem2  12832  pythagtrip  12849  pc2dvds  12896  pcz  12898  ctiunctlemfo  13053  unct  13056  sgrppropd  13489  mndpropd  13516  mhmeql  13568  mhmid  13695  mhmmnd  13696  mulgval  13702  issubg4m  13773  imasabl  13916  gsumfzconst  13921  dvdsrmul1  14109  unitgrp  14123  neissex  14882  restbasg  14885  tgrest  14886  restopnb  14898  cnptopco  14939  metequiv2  15213  xmettx  15227  metcnpi3  15234  mpomulcn  15283  fsumcncntop  15284  elcncf2  15291  cncfmet  15309  dedekindeulemuub  15334  dedekindeulemlu  15338  dedekindicclemuub  15343  dedekindicclemlu  15347  limccnpcntop  15392  dvmptfsum  15442  reeff1olem  15488  lgsquad3  15806  clwwlkccatlem  16209  nninfalllem1  16560  nninfnfiinf  16575  apdiff  16602