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  5904  tfrlem1  6460  phplem4dom  7031  phplem4on  7037  fisseneq  7104  suplub2ti  7176  omp1eomlem  7269  nnnninfeq  7303  nninfisol  7308  exmidontriim  7415  addcmpblnq  7562  mulcmpblnq  7563  ordpipqqs  7569  ltexnqq  7603  enq0tr  7629  addcmpblnq0  7638  mulcmpblnq0  7639  nnnq0lem1  7641  prssnql  7674  prmuloc  7761  prmuloc2  7762  mullocpr  7766  ltexprlemopu  7798  ltexprlemrl  7805  ltexprlemru  7807  addcanprleml  7809  addcanprlemu  7810  ltmprr  7837  archpr  7838  suplocexprlemloc  7916  addcmpblnr  7934  mulcmpblnrlemg  7935  mulcmpblnr  7936  ltsrprg  7942  srpospr  7978  axcaucvglemres  8094  axpre-suploclemres  8096  axpre-suploc  8097  negeu  8345  add20  8629  rimul  8740  apreap  8742  cru  8757  mulge0  8774  mulap0  8809  prodgt0  9007  ltmul12a  9015  ledivdiv  9045  lediv12a  9049  qapne  9842  qreccl  9845  xleaddadd  10091  ixxss12  10110  ioodisj  10197  fznlem  10245  elfz0fzfz0  10330  btwnzge0  10528  seqf1og  10751  mulexpzap  10809  leexp1a  10824  expnbnd  10893  hashennnuni  11009  zfz1iso  11071  seq3coll  11072  swrdswrdlem  11244  pfxccatin12lem3  11272  resqrexlemga  11542  sqrtsq  11563  abs3lem  11630  cau3lem  11633  minmax  11749  xrmaxiflemval  11769  xrminmax  11784  climcau  11866  summodclem2  11901  fsumrelem  11990  cvgratz  12051  mertenslemi1  12054  mertenslem2  12055  mertensabs  12056  fprodcl2lem  12124  fprodap0  12140  fprodrec  12148  fprodap0f  12155  fprodle  12159  dvdsle  12363  bitsfzo  12474  bezoutlemmain  12527  bezoutlemzz  12531  dfgcd3  12539  dvdsmulgcd  12554  lcmcllem  12597  lcmgcdlem  12607  ncoprmgcdne1b  12619  qredeu  12627  oddpwdclemxy  12699  oddpwdclemdc  12703  pythagtriplem2  12797  pythagtrip  12814  pc2dvds  12861  pcz  12863  ctiunctlemfo  13018  unct  13021  sgrppropd  13454  mndpropd  13481  mhmeql  13533  mhmid  13660  mhmmnd  13661  mulgval  13667  issubg4m  13738  imasabl  13881  gsumfzconst  13886  dvdsrmul1  14074  unitgrp  14088  neissex  14847  restbasg  14850  tgrest  14851  restopnb  14863  cnptopco  14904  metequiv2  15178  xmettx  15192  metcnpi3  15199  mpomulcn  15248  fsumcncntop  15249  elcncf2  15256  cncfmet  15274  dedekindeulemuub  15299  dedekindeulemlu  15303  dedekindicclemuub  15308  dedekindicclemlu  15312  limccnpcntop  15357  dvmptfsum  15407  reeff1olem  15453  lgsquad3  15771  nninfalllem1  16404  nninfnfiinf  16419  apdiff  16446