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  6002  tfrlemisucaccv  6596  tfr1onlemsucaccv  6612  tfrcllemsucaccv  6625  2omap  7318  addcmpblnq  7734  mulcmpblnq  7735  ordpipqqs  7741  nqnq0pi  7805  addcmpblnq0  7810  mulcmpblnq0  7811  addnq0mo  7814  mulnq0mo  7815  prarloclemcalc  7869  prarloc  7870  nqprl  7918  mullocpr  7938  distrlem4prl  7951  distrlem4pru  7952  ltprordil  7956  ltexprlemlol  7969  ltexprlemopu  7970  ltexprlemupu  7971  ltexprlemru  7979  cauappcvgprlemopl  8013  cauappcvgprlem2  8027  caucvgprlemopl  8036  caucvgprlem2  8047  caucvgprprlemexbt  8073  caucvgprprlem2  8077  suplocexprlemloc  8088  suplocexprlemub  8090  suplocexprlemlub  8091  addcmpblnr  8106  mulcmpblnrlemg  8107  mulcmpblnr  8108  prsrlem1  8109  addsrmo  8110  mulsrmo  8111  ltsrprg  8114  axmulcl  8233  recriota  8257  ltmul1  8921  divdivdivap  9044  divsubdivap  9059  ledivdiv  9221  lediv12a  9225  infssfzcldc  10671  infssfzledc  10672  suprzcl2dc  10676  exbtwnz  10687  qbtwnre  10693  ioom  10697  seq3caopr  10934  seqcaoprg  10935  leexp2r  11032  hashunlem  11246  hashfibclem  11284  wrd2ind  11497  recvguniq  11763  rsqrmo  11795  fsum2dlemstep  12203  expcnvre  12272  fprod2dlemstep  12391  bezout  12790  qredeu  12877  pw2dvdseu  12948  oddpwdclemndvds  12951  pcqmul  13084  pcadd  13121  pockthg  13138  grprida  13709  ghmpreima  14071  unitgrp  14425  islmodd  14631  lmodprop2d  14687  lsspropdg  14770  assapropd  15016  epttop  15193  restbasg  15271  iscnp4  15321  cnptopco  15325  blssps  15530  blss  15531  metequiv2  15599  xmetxpbl  15611  suplociccex  15728  dedekindicc  15736  limcimolemlt  15767  pellexlem3  16099  lgsquad2lem2  16213  2sqlem5  16250