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  5777  tfrlem1  6311  phplem4dom  6864  phplem4on  6869  fisseneq  6933  suplub2ti  7002  omp1eomlem  7095  nnnninfeq  7128  nninfisol  7133  exmidontriim  7226  addcmpblnq  7368  mulcmpblnq  7369  ordpipqqs  7375  ltexnqq  7409  enq0tr  7435  addcmpblnq0  7444  mulcmpblnq0  7445  nnnq0lem1  7447  prssnql  7480  prmuloc  7567  prmuloc2  7568  mullocpr  7572  ltexprlemopu  7604  ltexprlemrl  7611  ltexprlemru  7613  addcanprleml  7615  addcanprlemu  7616  ltmprr  7643  archpr  7644  suplocexprlemloc  7722  addcmpblnr  7740  mulcmpblnrlemg  7741  mulcmpblnr  7742  ltsrprg  7748  srpospr  7784  axcaucvglemres  7900  axpre-suploclemres  7902  axpre-suploc  7903  negeu  8150  add20  8433  rimul  8544  apreap  8546  cru  8561  mulge0  8578  mulap0  8613  prodgt0  8811  ltmul12a  8819  ledivdiv  8849  lediv12a  8853  qapne  9641  qreccl  9644  xleaddadd  9889  ixxss12  9908  ioodisj  9995  fznlem  10043  elfz0fzfz0  10128  btwnzge0  10302  mulexpzap  10562  leexp1a  10577  expnbnd  10646  hashennnuni  10761  zfz1iso  10823  seq3coll  10824  resqrexlemga  11034  sqrtsq  11055  abs3lem  11122  cau3lem  11125  minmax  11240  xrmaxiflemval  11260  xrminmax  11275  climcau  11357  summodclem2  11392  fsumrelem  11481  cvgratz  11542  mertenslemi1  11545  mertenslem2  11546  mertensabs  11547  fprodcl2lem  11615  fprodap0  11631  fprodrec  11639  fprodap0f  11646  fprodle  11650  dvdsle  11852  gcdsupex  11960  gcdsupcl  11961  bezoutlemmain  12001  bezoutlemzz  12005  dfgcd3  12013  dvdsmulgcd  12028  lcmcllem  12069  lcmgcdlem  12079  ncoprmgcdne1b  12091  qredeu  12099  oddpwdclemxy  12171  oddpwdclemdc  12175  pythagtriplem2  12268  pythagtrip  12285  pc2dvds  12331  pcz  12333  ctiunctlemfo  12442  unct  12445  mndpropd  12846  mhmeql  12881  mhmid  12984  mhmmnd  12985  mulgval  12991  issubg4m  13058  reldvdsrsrg  13266  dvdsrmul1  13276  unitgrp  13290  neissex  13704  restbasg  13707  tgrest  13708  restopnb  13720  cnptopco  13761  metequiv2  14035  xmettx  14049  metcnpi3  14056  fsumcncntop  14095  elcncf2  14100  cncfmet  14118  dedekindeulemuub  14134  dedekindeulemlu  14138  dedekindicclemuub  14143  dedekindicclemlu  14147  limccnpcntop  14183  reeff1olem  14231  nninfalllem1  14796  apdiff  14835