Theorem simprrr 546

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 495	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  5996  tfrlemisucaccv  6590  tfr1onlemsucaccv  6606  tfrcllemsucaccv  6619  2omap  7312  addcmpblnq  7728  mulcmpblnq  7729  ordpipqqs  7735  nqnq0pi  7799  addcmpblnq0  7804  mulcmpblnq0  7805  addnq0mo  7808  mulnq0mo  7809  prarloclemcalc  7863  prarloc  7864  nqprl  7912  mullocpr  7932  distrlem4prl  7945  distrlem4pru  7946  ltprordil  7950  ltexprlemlol  7963  ltexprlemopu  7964  ltexprlemupu  7965  ltexprlemru  7973  cauappcvgprlemopl  8007  cauappcvgprlem2  8021  caucvgprlemopl  8030  caucvgprlem2  8041  caucvgprprlemexbt  8067  caucvgprprlem2  8071  suplocexprlemloc  8082  suplocexprlemub  8084  suplocexprlemlub  8085  addcmpblnr  8100  mulcmpblnrlemg  8101  mulcmpblnr  8102  prsrlem1  8103  addsrmo  8104  mulsrmo  8105  ltsrprg  8108  axmulcl  8227  recriota  8251  ltmul1  8914  divdivdivap  9037  divsubdivap  9052  ledivdiv  9214  lediv12a  9218  infssfzcldc  10652  infssfzledc  10653  suprzcl2dc  10657  exbtwnz  10668  qbtwnre  10674  ioom  10678  seq3caopr  10915  seqcaoprg  10916  leexp2r  11013  hashunlem  11227  hashfibclem  11265  wrd2ind  11478  recvguniq  11744  rsqrmo  11776  fsum2dlemstep  12184  expcnvre  12253  fprod2dlemstep  12372  bezout  12771  qredeu  12858  pw2dvdseu  12929  oddpwdclemndvds  12932  pcqmul  13065  pcadd  13102  pockthg  13119  grprida  13690  ghmpreima  14052  unitgrp  14406  islmodd  14612  lmodprop2d  14668  lsspropdg  14751  assapropd  14997  epttop  15174  restbasg  15252  iscnp4  15302  cnptopco  15306  blssps  15511  blss  15512  metequiv2  15580  xmetxpbl  15592  suplociccex  15709  dedekindicc  15717  limcimolemlt  15748  pellexlem3  16076  lgsquad2lem2  16184  2sqlem5  16221