Theorem simprrl 541

Description: Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)

Assertion

Ref	Expression
simprrl	⊢ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃))) → 𝜒)

Proof of Theorem simprrl

Step	Hyp	Ref	Expression
1		simpl 109	. 2 ⊢ ((𝜒 ∧ 𝜃) → 𝜒)
2	1	ad2antll 491	1 ⊢ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃))) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 104

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

This theorem is referenced by:  dn1dc  969  imain  5443  tfrlemisucaccv  6569  tfrexlem  6578  tfr1onlemsucaccv  6585  tfrcllemsucaccv  6598  eroveu  6873  addcmpblnq  7698  mulcmpblnq  7699  ordpipqqs  7705  nqnq0pi  7769  addcmpblnq0  7774  mulcmpblnq0  7775  prarloclemcalc  7833  prarloc  7834  nqpru  7883  mullocpr  7902  distrlem4prl  7915  distrlem4pru  7916  ltprordil  7920  ltexprlemm  7931  ltexprlemopu  7934  ltexprlemupu  7935  ltexprlemru  7943  cauappcvgprlemopl  7977  cauappcvgprlem2  7991  caucvgprlemopl  8000  caucvgprlem2  8011  caucvgprprlemexbt  8037  caucvgprprlem2  8041  suplocexprlemloc  8052  suplocexprlemub  8054  suplocexprlemlub  8055  addcmpblnr  8070  mulcmpblnrlemg  8071  mulcmpblnr  8072  prsrlem1  8073  ltsrprg  8078  axmulcl  8197  ltmul1  8884  divdivdivap  9007  divmuleqap  9011  divsubdivap  9022  lt2mul2div  9173  ledivdiv  9184  lediv12a  9188  ssfzo12bi  10595  infssfzcldc  10621  infssfzledc  10622  suprzcl2dc  10626  exbtwnz  10637  qbtwnre  10643  ioom  10647  seq3caopr  10884  seqcaoprg  10885  leexp2r  10982  hashunlem  11196  hashfibclem  11234  wrd2ind  11443  recvguniq  11708  rsqrmo  11740  fsum2dlemstep  12148  expcnvre  12217  fprod2dlemstep  12336  bezout  12735  qredeu  12822  pw2dvdseu  12893  oddpwdclemdvds  12895  pcqmul  13029  pcadd  13066  pockthg  13083  grprida  13653  issubmd  13732  ghmpreima  14022  unitgrp  14364  lmodprop2d  14625  lsspropdg  14708  neiint  15139  restbasg  15162  iscnp4  15212  cnpnei  15213  cnptopco  15216  blssps  15421  blss  15422  metequiv2  15490  xmetxpbl  15502  suplociccex  15619  dedekindicc  15627  limcimolemlt  15658  pellexlem3  15976  lgsquad2lem2  16084  2sqlem5  16121