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  5932  tfrlemisucaccv  6486  tfr1onlemsucaccv  6502  tfrcllemsucaccv  6515  addcmpblnq  7580  mulcmpblnq  7581  ordpipqqs  7587  nqnq0pi  7651  addcmpblnq0  7656  mulcmpblnq0  7657  addnq0mo  7660  mulnq0mo  7661  prarloclemcalc  7715  prarloc  7716  nqprl  7764  mullocpr  7784  distrlem4prl  7797  distrlem4pru  7798  ltprordil  7802  ltexprlemlol  7815  ltexprlemopu  7816  ltexprlemupu  7817  ltexprlemru  7825  cauappcvgprlemopl  7859  cauappcvgprlem2  7873  caucvgprlemopl  7882  caucvgprlem2  7893  caucvgprprlemexbt  7919  caucvgprprlem2  7923  suplocexprlemloc  7934  suplocexprlemub  7936  suplocexprlemlub  7937  addcmpblnr  7952  mulcmpblnrlemg  7953  mulcmpblnr  7954  prsrlem1  7955  addsrmo  7956  mulsrmo  7957  ltsrprg  7960  axmulcl  8079  recriota  8103  ltmul1  8765  divdivdivap  8886  divsubdivap  8901  ledivdiv  9063  lediv12a  9067  suprzcl2dc  10492  exbtwnz  10503  qbtwnre  10509  ioom  10513  seq3caopr  10750  seqcaoprg  10751  leexp2r  10848  hashunlem  11060  wrd2ind  11297  recvguniq  11549  rsqrmo  11581  fsum2dlemstep  11988  expcnvre  12057  fprod2dlemstep  12176  bezout  12575  qredeu  12662  pw2dvdseu  12733  oddpwdclemndvds  12736  pcqmul  12869  pcadd  12906  pockthg  12923  grprida  13463  ghmpreima  13846  unitgrp  14123  islmodd  14300  lmodprop2d  14355  lsspropdg  14438  epttop  14807  restbasg  14885  iscnp4  14935  cnptopco  14939  blssps  15144  blss  15145  metequiv2  15213  xmetxpbl  15225  suplociccex  15342  dedekindicc  15350  limcimolemlt  15381  lgsquad2lem2  15804  2sqlem5  15841  2omap  16544