Theorem simprrr 529

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

Syntax hints:   → wi 4   ∧ wa 103

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

This theorem is referenced by:  fliftfun  5690  grpridd  5960  tfrlemisucaccv  6215  tfr1onlemsucaccv  6231  tfrcllemsucaccv  6244  addcmpblnq  7168  mulcmpblnq  7169  ordpipqqs  7175  nqnq0pi  7239  addcmpblnq0  7244  mulcmpblnq0  7245  addnq0mo  7248  mulnq0mo  7249  prarloclemcalc  7303  prarloc  7304  nqprl  7352  mullocpr  7372  distrlem4prl  7385  distrlem4pru  7386  ltprordil  7390  ltexprlemlol  7403  ltexprlemopu  7404  ltexprlemupu  7405  ltexprlemru  7413  cauappcvgprlemopl  7447  cauappcvgprlem2  7461  caucvgprlemopl  7470  caucvgprlem2  7481  caucvgprprlemexbt  7507  caucvgprprlem2  7511  suplocexprlemloc  7522  suplocexprlemub  7524  suplocexprlemlub  7525  addcmpblnr  7540  mulcmpblnrlemg  7541  mulcmpblnr  7542  prsrlem1  7543  addsrmo  7544  mulsrmo  7545  ltsrprg  7548  axmulcl  7667  recriota  7691  ltmul1  8347  divdivdivap  8466  divsubdivap  8481  ledivdiv  8641  lediv12a  8645  exbtwnz  10021  qbtwnre  10027  ioom  10031  seq3caopr  10249  leexp2r  10340  hashunlem  10543  recvguniq  10760  rsqrmo  10792  fsum2dlemstep  11196  expcnvre  11265  bezout  11688  qredeu  11767  pw2dvdseu  11835  oddpwdclemndvds  11838  epttop  12248  restbasg  12326  iscnp4  12376  cnptopco  12380  blssps  12585  blss  12586  metequiv2  12654  xmetxpbl  12666  suplociccex  12761  dedekindicc  12769  limcimolemlt  12791