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  5926  tfrlemisucaccv  6477  tfr1onlemsucaccv  6493  tfrcllemsucaccv  6506  addcmpblnq  7562  mulcmpblnq  7563  ordpipqqs  7569  nqnq0pi  7633  addcmpblnq0  7638  mulcmpblnq0  7639  addnq0mo  7642  mulnq0mo  7643  prarloclemcalc  7697  prarloc  7698  nqprl  7746  mullocpr  7766  distrlem4prl  7779  distrlem4pru  7780  ltprordil  7784  ltexprlemlol  7797  ltexprlemopu  7798  ltexprlemupu  7799  ltexprlemru  7807  cauappcvgprlemopl  7841  cauappcvgprlem2  7855  caucvgprlemopl  7864  caucvgprlem2  7875  caucvgprprlemexbt  7901  caucvgprprlem2  7905  suplocexprlemloc  7916  suplocexprlemub  7918  suplocexprlemlub  7919  addcmpblnr  7934  mulcmpblnrlemg  7935  mulcmpblnr  7936  prsrlem1  7937  addsrmo  7938  mulsrmo  7939  ltsrprg  7942  axmulcl  8061  recriota  8085  ltmul1  8747  divdivdivap  8868  divsubdivap  8883  ledivdiv  9045  lediv12a  9049  suprzcl2dc  10467  exbtwnz  10478  qbtwnre  10484  ioom  10488  seq3caopr  10725  seqcaoprg  10726  leexp2r  10823  hashunlem  11034  wrd2ind  11263  recvguniq  11514  rsqrmo  11546  fsum2dlemstep  11953  expcnvre  12022  fprod2dlemstep  12141  bezout  12540  qredeu  12627  pw2dvdseu  12698  oddpwdclemndvds  12701  pcqmul  12834  pcadd  12871  pockthg  12888  grprida  13428  ghmpreima  13811  unitgrp  14088  islmodd  14265  lmodprop2d  14320  lsspropdg  14403  epttop  14772  restbasg  14850  iscnp4  14900  cnptopco  14904  blssps  15109  blss  15110  metequiv2  15178  xmetxpbl  15190  suplociccex  15307  dedekindicc  15315  limcimolemlt  15346  lgsquad2lem2  15769  2sqlem5  15806  2omap  16388