Theorem simprrr 529

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 109	. 2 ⊢ ((𝜒 ∧ 𝜃) → 𝜃)
2	1	ad2antll 482	1 ⊢ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃))) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  fliftfun  5697  grpridd  5967  tfrlemisucaccv  6222  tfr1onlemsucaccv  6238  tfrcllemsucaccv  6251  addcmpblnq  7175  mulcmpblnq  7176  ordpipqqs  7182  nqnq0pi  7246  addcmpblnq0  7251  mulcmpblnq0  7252  addnq0mo  7255  mulnq0mo  7256  prarloclemcalc  7310  prarloc  7311  nqprl  7359  mullocpr  7379  distrlem4prl  7392  distrlem4pru  7393  ltprordil  7397  ltexprlemlol  7410  ltexprlemopu  7411  ltexprlemupu  7412  ltexprlemru  7420  cauappcvgprlemopl  7454  cauappcvgprlem2  7468  caucvgprlemopl  7477  caucvgprlem2  7488  caucvgprprlemexbt  7514  caucvgprprlem2  7518  suplocexprlemloc  7529  suplocexprlemub  7531  suplocexprlemlub  7532  addcmpblnr  7547  mulcmpblnrlemg  7548  mulcmpblnr  7549  prsrlem1  7550  addsrmo  7551  mulsrmo  7552  ltsrprg  7555  axmulcl  7674  recriota  7698  ltmul1  8354  divdivdivap  8473  divsubdivap  8488  ledivdiv  8648  lediv12a  8652  exbtwnz  10028  qbtwnre  10034  ioom  10038  seq3caopr  10256  leexp2r  10347  hashunlem  10550  recvguniq  10767  rsqrmo  10799  fsum2dlemstep  11203  expcnvre  11272  bezout  11699  qredeu  11778  pw2dvdseu  11846  oddpwdclemndvds  11849  epttop  12259  restbasg  12337  iscnp4  12387  cnptopco  12391  blssps  12596  blss  12597  metequiv2  12665  xmetxpbl  12677  suplociccex  12772  dedekindicc  12780  limcimolemlt  12802