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  5792  tfrlemisucaccv  6321  tfr1onlemsucaccv  6337  tfrcllemsucaccv  6350  addcmpblnq  7361  mulcmpblnq  7362  ordpipqqs  7368  nqnq0pi  7432  addcmpblnq0  7437  mulcmpblnq0  7438  addnq0mo  7441  mulnq0mo  7442  prarloclemcalc  7496  prarloc  7497  nqprl  7545  mullocpr  7565  distrlem4prl  7578  distrlem4pru  7579  ltprordil  7583  ltexprlemlol  7596  ltexprlemopu  7597  ltexprlemupu  7598  ltexprlemru  7606  cauappcvgprlemopl  7640  cauappcvgprlem2  7654  caucvgprlemopl  7663  caucvgprlem2  7674  caucvgprprlemexbt  7700  caucvgprprlem2  7704  suplocexprlemloc  7715  suplocexprlemub  7717  suplocexprlemlub  7718  addcmpblnr  7733  mulcmpblnrlemg  7734  mulcmpblnr  7735  prsrlem1  7736  addsrmo  7737  mulsrmo  7738  ltsrprg  7741  axmulcl  7860  recriota  7884  ltmul1  8543  divdivdivap  8664  divsubdivap  8679  ledivdiv  8841  lediv12a  8845  exbtwnz  10244  qbtwnre  10250  ioom  10254  seq3caopr  10476  leexp2r  10567  hashunlem  10775  recvguniq  10995  rsqrmo  11027  fsum2dlemstep  11433  expcnvre  11502  fprod2dlemstep  11621  suprzcl2dc  11946  bezout  12002  qredeu  12087  pw2dvdseu  12158  oddpwdclemndvds  12161  pcqmul  12293  pcadd  12329  pockthg  12345  grpridd  12736  unitgrp  13184  epttop  13372  restbasg  13450  iscnp4  13500  cnptopco  13504  blssps  13709  blss  13710  metequiv2  13778  xmetxpbl  13790  suplociccex  13885  dedekindicc  13893  limcimolemlt  13915  2sqlem5  14237