Theorem simprrl 539

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  962  imain  5341  tfrlemisucaccv  6392  tfrexlem  6401  tfr1onlemsucaccv  6408  tfrcllemsucaccv  6421  eroveu  6694  addcmpblnq  7453  mulcmpblnq  7454  ordpipqqs  7460  nqnq0pi  7524  addcmpblnq0  7529  mulcmpblnq0  7530  prarloclemcalc  7588  prarloc  7589  nqpru  7638  mullocpr  7657  distrlem4prl  7670  distrlem4pru  7671  ltprordil  7675  ltexprlemm  7686  ltexprlemopu  7689  ltexprlemupu  7690  ltexprlemru  7698  cauappcvgprlemopl  7732  cauappcvgprlem2  7746  caucvgprlemopl  7755  caucvgprlem2  7766  caucvgprprlemexbt  7792  caucvgprprlem2  7796  suplocexprlemloc  7807  suplocexprlemub  7809  suplocexprlemlub  7810  addcmpblnr  7825  mulcmpblnrlemg  7826  mulcmpblnr  7827  prsrlem1  7828  ltsrprg  7833  axmulcl  7952  ltmul1  8638  divdivdivap  8759  divmuleqap  8763  divsubdivap  8774  lt2mul2div  8925  ledivdiv  8936  lediv12a  8940  ssfzo12bi  10320  suprzcl2dc  10348  exbtwnz  10359  qbtwnre  10365  ioom  10369  seq3caopr  10606  seqcaoprg  10607  leexp2r  10704  hashunlem  10915  recvguniq  11179  rsqrmo  11211  fsum2dlemstep  11618  expcnvre  11687  fprod2dlemstep  11806  bezout  12205  qredeu  12292  pw2dvdseu  12363  oddpwdclemdvds  12365  pcqmul  12499  pcadd  12536  pockthg  12553  grprida  13091  issubmd  13178  ghmpreima  13474  unitgrp  13750  lmodprop2d  13982  lsspropdg  14065  neiint  14467  restbasg  14490  iscnp4  14540  cnpnei  14541  cnptopco  14544  blssps  14749  blss  14750  metequiv2  14818  xmetxpbl  14830  suplociccex  14947  dedekindicc  14955  limcimolemlt  14986  lgsquad2lem2  15409  2sqlem5  15446