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  5814  tfrlemisucaccv  6345  tfr1onlemsucaccv  6361  tfrcllemsucaccv  6374  addcmpblnq  7386  mulcmpblnq  7387  ordpipqqs  7393  nqnq0pi  7457  addcmpblnq0  7462  mulcmpblnq0  7463  addnq0mo  7466  mulnq0mo  7467  prarloclemcalc  7521  prarloc  7522  nqprl  7570  mullocpr  7590  distrlem4prl  7603  distrlem4pru  7604  ltprordil  7608  ltexprlemlol  7621  ltexprlemopu  7622  ltexprlemupu  7623  ltexprlemru  7631  cauappcvgprlemopl  7665  cauappcvgprlem2  7679  caucvgprlemopl  7688  caucvgprlem2  7699  caucvgprprlemexbt  7725  caucvgprprlem2  7729  suplocexprlemloc  7740  suplocexprlemub  7742  suplocexprlemlub  7743  addcmpblnr  7758  mulcmpblnrlemg  7759  mulcmpblnr  7760  prsrlem1  7761  addsrmo  7762  mulsrmo  7763  ltsrprg  7766  axmulcl  7885  recriota  7909  ltmul1  8569  divdivdivap  8690  divsubdivap  8705  ledivdiv  8867  lediv12a  8871  exbtwnz  10271  qbtwnre  10277  ioom  10281  seq3caopr  10503  leexp2r  10594  hashunlem  10804  recvguniq  11024  rsqrmo  11056  fsum2dlemstep  11462  expcnvre  11531  fprod2dlemstep  11650  suprzcl2dc  11976  bezout  12032  qredeu  12117  pw2dvdseu  12188  oddpwdclemndvds  12191  pcqmul  12323  pcadd  12359  pockthg  12375  grprida  12836  ghmpreima  13173  unitgrp  13434  islmodd  13577  lmodprop2d  13632  lsspropdg  13715  epttop  13994  restbasg  14072  iscnp4  14122  cnptopco  14126  blssps  14331  blss  14332  metequiv2  14400  xmetxpbl  14412  suplociccex  14507  dedekindicc  14515  limcimolemlt  14537  2sqlem5  14870