Theorem simplll 539

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 492	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  547  f1imass  5974  suppcofn  6500  tfrlem1  6573  phplem4dom  7157  phplem4on  7163  fisseneq  7236  suplub2ti  7335  omp1eomlem  7428  nnnninfeq  7462  nninfisol  7467  exmidontriim  7575  addcmpblnq  7728  mulcmpblnq  7729  ordpipqqs  7735  ltexnqq  7769  enq0tr  7795  addcmpblnq0  7804  mulcmpblnq0  7805  nnnq0lem1  7807  prssnql  7840  prmuloc  7927  prmuloc2  7928  mullocpr  7932  ltexprlemopu  7964  ltexprlemrl  7971  ltexprlemru  7973  addcanprleml  7975  addcanprlemu  7976  ltmprr  8003  archpr  8004  suplocexprlemloc  8082  addcmpblnr  8100  mulcmpblnrlemg  8101  mulcmpblnr  8102  ltsrprg  8108  srpospr  8144  axcaucvglemres  8260  axpre-suploclemres  8262  axpre-suploc  8263  negeu  8511  add20  8796  rimul  8907  apreap  8909  cru  8924  mulge0  8941  mulap0  8976  prodgt0  9176  ltmul12a  9184  ledivdiv  9214  lediv12a  9218  qapne  10022  qreccl  10025  xleaddadd  10272  ixxss12  10291  ioodisj  10378  fznlem  10428  elfz0fzfz0  10516  btwnzge0  10718  seqf1og  10941  mulexpzap  10999  leexp1a  11014  expnbnd  11084  hashennnuni  11201  hashf1lem2  11269  zfz1iso  11276  seq3coll  11277  swrdswrdlem  11459  pfxccatin12lem3  11487  resqrexlemga  11772  sqrtsq  11793  abs3lem  11860  cau3lem  11863  minmax  11979  xrmaxiflemval  11999  xrminmax  12014  climcau  12096  summodclem2  12132  fsumrelem  12221  cvgratz  12282  mertenslemi1  12285  mertenslem2  12286  mertensabs  12287  fprodcl2lem  12355  fprodap0  12371  fprodrec  12379  fprodap0f  12386  fprodle  12390  dvdsle  12594  bitsfzo  12705  bezoutlemmain  12758  bezoutlemzz  12762  dfgcd3  12770  dvdsmulgcd  12785  lcmcllem  12828  lcmgcdlem  12838  ncoprmgcdne1b  12850  qredeu  12858  oddpwdclemxy  12930  oddpwdclemdc  12934  pythagtriplem2  13028  pythagtrip  13045  pc2dvds  13092  pcz  13094  ctiunctlemfo  13313  unct  13316  sgrppropd  13711  mndpropd  13736  mhmeql  13782  mhmid  13901  mhmmnd  13902  mulgval  13908  issubg4m  13979  imasabl  14123  gzsumconst  14126  gsumzfi  14141  gsummptfidmadd  14144  dvdsrmul1  14392  unitgrp  14406  aprlring  14583  gsumfsum  14906  issubassa2  15018  neissex  15249  restbasg  15252  tgrest  15253  restopnb  15265  cnptopco  15306  metequiv2  15580  xmettx  15594  metcnpi3  15601  mpomulcn  15650  fsumcncntop  15651  elcncf2  15658  cncfmet  15676  dedekindeulemuub  15701  dedekindeulemlu  15705  dedekindicclemuub  15710  dedekindicclemlu  15714  limccnpcntop  15759  dvmptfsum  15809  reeff1olem  15855  lgsquad3  16186  clwwlkccatlem  16624  nninfalllem1  17025  nninfnfiinf  17040  apdiff  17071