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  5810  tfrlemisucaccv  6340  tfr1onlemsucaccv  6356  tfrcllemsucaccv  6369  addcmpblnq  7380  mulcmpblnq  7381  ordpipqqs  7387  nqnq0pi  7451  addcmpblnq0  7456  mulcmpblnq0  7457  addnq0mo  7460  mulnq0mo  7461  prarloclemcalc  7515  prarloc  7516  nqprl  7564  mullocpr  7584  distrlem4prl  7597  distrlem4pru  7598  ltprordil  7602  ltexprlemlol  7615  ltexprlemopu  7616  ltexprlemupu  7617  ltexprlemru  7625  cauappcvgprlemopl  7659  cauappcvgprlem2  7673  caucvgprlemopl  7682  caucvgprlem2  7693  caucvgprprlemexbt  7719  caucvgprprlem2  7723  suplocexprlemloc  7734  suplocexprlemub  7736  suplocexprlemlub  7737  addcmpblnr  7752  mulcmpblnrlemg  7753  mulcmpblnr  7754  prsrlem1  7755  addsrmo  7756  mulsrmo  7757  ltsrprg  7760  axmulcl  7879  recriota  7903  ltmul1  8563  divdivdivap  8684  divsubdivap  8699  ledivdiv  8861  lediv12a  8865  exbtwnz  10265  qbtwnre  10271  ioom  10275  seq3caopr  10497  leexp2r  10588  hashunlem  10798  recvguniq  11018  rsqrmo  11050  fsum2dlemstep  11456  expcnvre  11525  fprod2dlemstep  11644  suprzcl2dc  11970  bezout  12026  qredeu  12111  pw2dvdseu  12182  oddpwdclemndvds  12185  pcqmul  12317  pcadd  12353  pockthg  12369  grprida  12825  unitgrp  13364  islmodd  13482  lmodprop2d  13537  lsspropdg  13620  epttop  13886  restbasg  13964  iscnp4  14014  cnptopco  14018  blssps  14223  blss  14224  metequiv2  14292  xmetxpbl  14304  suplociccex  14399  dedekindicc  14407  limcimolemlt  14429  2sqlem5  14762