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  5797  tfrlemisucaccv  6326  tfr1onlemsucaccv  6342  tfrcllemsucaccv  6355  addcmpblnq  7366  mulcmpblnq  7367  ordpipqqs  7373  nqnq0pi  7437  addcmpblnq0  7442  mulcmpblnq0  7443  addnq0mo  7446  mulnq0mo  7447  prarloclemcalc  7501  prarloc  7502  nqprl  7550  mullocpr  7570  distrlem4prl  7583  distrlem4pru  7584  ltprordil  7588  ltexprlemlol  7601  ltexprlemopu  7602  ltexprlemupu  7603  ltexprlemru  7611  cauappcvgprlemopl  7645  cauappcvgprlem2  7659  caucvgprlemopl  7668  caucvgprlem2  7679  caucvgprprlemexbt  7705  caucvgprprlem2  7709  suplocexprlemloc  7720  suplocexprlemub  7722  suplocexprlemlub  7723  addcmpblnr  7738  mulcmpblnrlemg  7739  mulcmpblnr  7740  prsrlem1  7741  addsrmo  7742  mulsrmo  7743  ltsrprg  7746  axmulcl  7865  recriota  7889  ltmul1  8549  divdivdivap  8670  divsubdivap  8685  ledivdiv  8847  lediv12a  8851  exbtwnz  10251  qbtwnre  10257  ioom  10261  seq3caopr  10483  leexp2r  10574  hashunlem  10784  recvguniq  11004  rsqrmo  11036  fsum2dlemstep  11442  expcnvre  11511  fprod2dlemstep  11630  suprzcl2dc  11956  bezout  12012  qredeu  12097  pw2dvdseu  12168  oddpwdclemndvds  12171  pcqmul  12303  pcadd  12339  pockthg  12355  grpridd  12806  unitgrp  13285  islmodd  13383  lmodprop2d  13438  epttop  13593  restbasg  13671  iscnp4  13721  cnptopco  13725  blssps  13930  blss  13931  metequiv2  13999  xmetxpbl  14011  suplociccex  14106  dedekindicc  14114  limcimolemlt  14136  2sqlem5  14469