Theorem simprrr 512

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 109	. 2 ⊢ ((𝜒 ∧ 𝜃) → 𝜃)
2	1	ad2antll 480	1 ⊢ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃))) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  fliftfun  5649  grpridd  5919  tfrlemisucaccv  6174  tfr1onlemsucaccv  6190  tfrcllemsucaccv  6203  addcmpblnq  7117  mulcmpblnq  7118  ordpipqqs  7124  nqnq0pi  7188  addcmpblnq0  7193  mulcmpblnq0  7194  addnq0mo  7197  mulnq0mo  7198  prarloclemcalc  7252  prarloc  7253  nqprl  7301  mullocpr  7321  distrlem4prl  7334  distrlem4pru  7335  ltprordil  7339  ltexprlemlol  7352  ltexprlemopu  7353  ltexprlemupu  7354  ltexprlemru  7362  cauappcvgprlemopl  7396  cauappcvgprlem2  7410  caucvgprlemopl  7419  caucvgprlem2  7430  caucvgprprlemexbt  7456  caucvgprprlem2  7460  addcmpblnr  7476  mulcmpblnrlemg  7477  mulcmpblnr  7478  prsrlem1  7479  addsrmo  7480  mulsrmo  7481  ltsrprg  7484  axmulcl  7595  recriota  7619  ltmul1  8266  divdivdivap  8380  divsubdivap  8395  ledivdiv  8552  lediv12a  8556  exbtwnz  9915  qbtwnre  9921  ioom  9925  seq3caopr  10143  leexp2r  10234  hashunlem  10437  recvguniq  10653  rsqrmo  10685  fsum2dlemstep  11089  expcnvre  11158  bezout  11539  qredeu  11618  pw2dvdseu  11685  oddpwdclemndvds  11688  epttop  12096  restbasg  12174  iscnp4  12223  cnptopco  12227  blssps  12410  blss  12411  metequiv2  12479  xmetxpbl  12491  limcimolemlt  12583