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  5893  tfrlemisucaccv  6441  tfr1onlemsucaccv  6457  tfrcllemsucaccv  6470  addcmpblnq  7522  mulcmpblnq  7523  ordpipqqs  7529  nqnq0pi  7593  addcmpblnq0  7598  mulcmpblnq0  7599  addnq0mo  7602  mulnq0mo  7603  prarloclemcalc  7657  prarloc  7658  nqprl  7706  mullocpr  7726  distrlem4prl  7739  distrlem4pru  7740  ltprordil  7744  ltexprlemlol  7757  ltexprlemopu  7758  ltexprlemupu  7759  ltexprlemru  7767  cauappcvgprlemopl  7801  cauappcvgprlem2  7815  caucvgprlemopl  7824  caucvgprlem2  7835  caucvgprprlemexbt  7861  caucvgprprlem2  7865  suplocexprlemloc  7876  suplocexprlemub  7878  suplocexprlemlub  7879  addcmpblnr  7894  mulcmpblnrlemg  7895  mulcmpblnr  7896  prsrlem1  7897  addsrmo  7898  mulsrmo  7899  ltsrprg  7902  axmulcl  8021  recriota  8045  ltmul1  8707  divdivdivap  8828  divsubdivap  8843  ledivdiv  9005  lediv12a  9009  suprzcl2dc  10426  exbtwnz  10437  qbtwnre  10443  ioom  10447  seq3caopr  10684  seqcaoprg  10685  leexp2r  10782  hashunlem  10993  wrd2ind  11221  recvguniq  11472  rsqrmo  11504  fsum2dlemstep  11911  expcnvre  11980  fprod2dlemstep  12099  bezout  12498  qredeu  12585  pw2dvdseu  12656  oddpwdclemndvds  12659  pcqmul  12792  pcadd  12829  pockthg  12846  grprida  13386  ghmpreima  13769  unitgrp  14045  islmodd  14222  lmodprop2d  14277  lsspropdg  14360  epttop  14729  restbasg  14807  iscnp4  14857  cnptopco  14861  blssps  15066  blss  15067  metequiv2  15135  xmetxpbl  15147  suplociccex  15264  dedekindicc  15272  limcimolemlt  15303  lgsquad2lem2  15726  2sqlem5  15763  2omap  16270