Theorem simprrr 542

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  5971  tfrlemisucaccv  6558  tfr1onlemsucaccv  6574  tfrcllemsucaccv  6587  2omap  7271  addcmpblnq  7687  mulcmpblnq  7688  ordpipqqs  7694  nqnq0pi  7758  addcmpblnq0  7763  mulcmpblnq0  7764  addnq0mo  7767  mulnq0mo  7768  prarloclemcalc  7822  prarloc  7823  nqprl  7871  mullocpr  7891  distrlem4prl  7904  distrlem4pru  7905  ltprordil  7909  ltexprlemlol  7922  ltexprlemopu  7923  ltexprlemupu  7924  ltexprlemru  7932  cauappcvgprlemopl  7966  cauappcvgprlem2  7980  caucvgprlemopl  7989  caucvgprlem2  8000  caucvgprprlemexbt  8026  caucvgprprlem2  8030  suplocexprlemloc  8041  suplocexprlemub  8043  suplocexprlemlub  8044  addcmpblnr  8059  mulcmpblnrlemg  8060  mulcmpblnr  8061  prsrlem1  8062  addsrmo  8063  mulsrmo  8064  ltsrprg  8067  axmulcl  8186  recriota  8210  ltmul1  8871  divdivdivap  8992  divsubdivap  9007  ledivdiv  9169  lediv12a  9173  suprzcl2dc  10606  exbtwnz  10617  qbtwnre  10623  ioom  10627  seq3caopr  10864  seqcaoprg  10865  leexp2r  10962  hashunlem  11176  hashfibclem  11214  wrd2ind  11423  recvguniq  11688  rsqrmo  11720  fsum2dlemstep  12128  expcnvre  12197  fprod2dlemstep  12316  bezout  12715  qredeu  12802  pw2dvdseu  12873  oddpwdclemndvds  12876  pcqmul  13009  pcadd  13046  pockthg  13063  grprida  13621  ghmpreima  14004  unitgrp  14283  islmodd  14490  lmodprop2d  14545  lsspropdg  14628  epttop  15004  restbasg  15082  iscnp4  15132  cnptopco  15136  blssps  15341  blss  15342  metequiv2  15410  xmetxpbl  15422  suplociccex  15539  dedekindicc  15547  limcimolemlt  15578  pellexlem3  15896  lgsquad2lem2  16004  2sqlem5  16041