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  8922  divdivdivap  9045  divsubdivap  9060  ledivdiv  9222  lediv12a  9226  infssfzcldc  10679  infssfzledc  10680  suprzcl2dc  10684  exbtwnz  10695  qbtwnre  10701  ioom  10705  seq3caopr  10945  seqcaoprg  10946  leexp2r  11043  hashunlem  11258  hashfibclem  11296  wrd2ind  11509  recvguniq  11775  rsqrmo  11807  fsum2dlemstep  12217  expcnvre  12286  fprod2dlemstep  12405  bezout  12804  qredeu  12891  pwbdvdseu  12963  nnmaxpwlemndvds  12966  nnmaxpwlemparts  12968  pcqmul  13102  pcadd  13139  pockthg  13156  grprida  13756  ghmpreima  14118  unitgrp  14472  islmodd  14678  lmodprop2d  14734  lsspropdg  14817  assapropd  15063  epttop  15240  restbasg  15318  iscnp4  15368  cnptopco  15372  blssps  15577  blss  15578  metequiv2  15646  xmetxpbl  15658  suplociccex  15775  dedekindicc  15783  limcimolemlt  15814  pellexlem3  16150  lgsquad2lem2  16320  2sqlem5  16357