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 ⊢ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃))) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  fliftfun  6005  tfrlemisucaccv  6600  tfr1onlemsucaccv  6616  tfrcllemsucaccv  6629  2omap  7325  addcmpblnq  7741  mulcmpblnq  7742  ordpipqqs  7748  nqnq0pi  7812  addcmpblnq0  7817  mulcmpblnq0  7818  addnq0mo  7821  mulnq0mo  7822  prarloclemcalc  7876  prarloc  7877  nqprl  7925  mullocpr  7945  distrlem4prl  7958  distrlem4pru  7959  ltprordil  7963  ltexprlemlol  7976  ltexprlemopu  7977  ltexprlemupu  7978  ltexprlemru  7986  cauappcvgprlemopl  8020  cauappcvgprlem2  8034  caucvgprlemopl  8043  caucvgprlem2  8054  caucvgprprlemexbt  8080  caucvgprprlem2  8084  suplocexprlemloc  8095  suplocexprlemub  8097  suplocexprlemlub  8098  addcmpblnr  8113  mulcmpblnrlemg  8114  mulcmpblnr  8115  prsrlem1  8116  addsrmo  8117  mulsrmo  8118  ltsrprg  8121  axmulcl  8240  recriota  8264  ltmul1  8929  divdivdivap  9052  divsubdivap  9067  ledivdiv  9229  lediv12a  9233  infssfzcldc  10687  infssfzledc  10688  suprzcl2dc  10692  exbtwnz  10703  qbtwnre  10709  ioom  10713  seq3caopr  10954  seqcaoprg  10955  leexp2r  11052  hashunlem  11267  hashfibclem  11305  wrd2ind  11518  recvguniq  11784  rsqrmo  11816  fsum2dlemstep  12227  expcnvre  12296  fprod2dlemstep  12415  bezout  12814  qredeu  12901  pwbdvdseu  12973  nnmaxpwlemndvds  12976  nnmaxpwlemparts  12978  pcqmul  13112  pcadd  13149  pockthg  13166  grprida  13767  ghmpreima  14129  unitgrp  14533  islmodd  14739  lmodprop2d  14795  lsspropdg  14878  assapropd  15124  epttop  15328  restbasg  15406  iscnp4  15456  cnptopco  15460  blssps  15665  blss  15666  metequiv2  15734  xmetxpbl  15746  suplociccex  15863  dedekindicc  15871  limcimolemlt  15902  pellexlem3  16243  lgsquad2lem2  16418  2sqlem5  16455