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  7319  addcmpblnq  7735  mulcmpblnq  7736  ordpipqqs  7742  nqnq0pi  7806  addcmpblnq0  7811  mulcmpblnq0  7812  addnq0mo  7815  mulnq0mo  7816  prarloclemcalc  7870  prarloc  7871  nqprl  7919  mullocpr  7939  distrlem4prl  7952  distrlem4pru  7953  ltprordil  7957  ltexprlemlol  7970  ltexprlemopu  7971  ltexprlemupu  7972  ltexprlemru  7980  cauappcvgprlemopl  8014  cauappcvgprlem2  8028  caucvgprlemopl  8037  caucvgprlem2  8048  caucvgprprlemexbt  8074  caucvgprprlem2  8078  suplocexprlemloc  8089  suplocexprlemub  8091  suplocexprlemlub  8092  addcmpblnr  8107  mulcmpblnrlemg  8108  mulcmpblnr  8109  prsrlem1  8110  addsrmo  8111  mulsrmo  8112  ltsrprg  8115  axmulcl  8234  recriota  8258  ltmul1  8923  divdivdivap  9046  divsubdivap  9061  ledivdiv  9223  lediv12a  9227  infssfzcldc  10680  infssfzledc  10681  suprzcl2dc  10685  exbtwnz  10696  qbtwnre  10702  ioom  10706  seq3caopr  10947  seqcaoprg  10948  leexp2r  11045  hashunlem  11260  hashfibclem  11298  wrd2ind  11511  recvguniq  11777  rsqrmo  11809  fsum2dlemstep  12220  expcnvre  12289  fprod2dlemstep  12408  bezout  12807  qredeu  12894  pwbdvdseu  12966  nnmaxpwlemndvds  12969  nnmaxpwlemparts  12971  pcqmul  13105  pcadd  13142  pockthg  13159  grprida  13760  ghmpreima  14122  unitgrp  14507  islmodd  14713  lmodprop2d  14769  lsspropdg  14852  assapropd  15098  epttop  15282  restbasg  15360  iscnp4  15410  cnptopco  15414  blssps  15619  blss  15620  metequiv2  15688  xmetxpbl  15700  suplociccex  15817  dedekindicc  15825  limcimolemlt  15856  pellexlem3  16197  lgsquad2lem2  16372  2sqlem5  16409