Theorem simprrr 540

Description: Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)

Assertion

Ref	Expression
simprrr	⊢ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃))) → 𝜃)

Proof of Theorem simprrr

Step	Hyp	Ref	Expression
1		simpr 110	. 2 ⊢ ((𝜒 ∧ 𝜃) → 𝜃)
2	1	ad2antll 491	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:  fliftfun  5818  tfrlemisucaccv  6350  tfr1onlemsucaccv  6366  tfrcllemsucaccv  6379  addcmpblnq  7396  mulcmpblnq  7397  ordpipqqs  7403  nqnq0pi  7467  addcmpblnq0  7472  mulcmpblnq0  7473  addnq0mo  7476  mulnq0mo  7477  prarloclemcalc  7531  prarloc  7532  nqprl  7580  mullocpr  7600  distrlem4prl  7613  distrlem4pru  7614  ltprordil  7618  ltexprlemlol  7631  ltexprlemopu  7632  ltexprlemupu  7633  ltexprlemru  7641  cauappcvgprlemopl  7675  cauappcvgprlem2  7689  caucvgprlemopl  7698  caucvgprlem2  7709  caucvgprprlemexbt  7735  caucvgprprlem2  7739  suplocexprlemloc  7750  suplocexprlemub  7752  suplocexprlemlub  7753  addcmpblnr  7768  mulcmpblnrlemg  7769  mulcmpblnr  7770  prsrlem1  7771  addsrmo  7772  mulsrmo  7773  ltsrprg  7776  axmulcl  7895  recriota  7919  ltmul1  8579  divdivdivap  8700  divsubdivap  8715  ledivdiv  8877  lediv12a  8881  exbtwnz  10281  qbtwnre  10287  ioom  10291  seq3caopr  10514  leexp2r  10605  hashunlem  10816  recvguniq  11036  rsqrmo  11068  fsum2dlemstep  11474  expcnvre  11543  fprod2dlemstep  11662  suprzcl2dc  11988  bezout  12044  qredeu  12129  pw2dvdseu  12200  oddpwdclemndvds  12203  pcqmul  12335  pcadd  12372  pockthg  12389  grprida  12863  ghmpreima  13205  unitgrp  13466  islmodd  13609  lmodprop2d  13664  lsspropdg  13747  epttop  14047  restbasg  14125  iscnp4  14175  cnptopco  14179  blssps  14384  blss  14385  metequiv2  14453  xmetxpbl  14465  suplociccex  14560  dedekindicc  14568  limcimolemlt  14590  2sqlem5  14924