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  968  imain  5414  tfrlemisucaccv  6496  tfrexlem  6505  tfr1onlemsucaccv  6512  tfrcllemsucaccv  6525  eroveu  6800  addcmpblnq  7592  mulcmpblnq  7593  ordpipqqs  7599  nqnq0pi  7663  addcmpblnq0  7668  mulcmpblnq0  7669  prarloclemcalc  7727  prarloc  7728  nqpru  7777  mullocpr  7796  distrlem4prl  7809  distrlem4pru  7810  ltprordil  7814  ltexprlemm  7825  ltexprlemopu  7828  ltexprlemupu  7829  ltexprlemru  7837  cauappcvgprlemopl  7871  cauappcvgprlem2  7885  caucvgprlemopl  7894  caucvgprlem2  7905  caucvgprprlemexbt  7931  caucvgprprlem2  7935  suplocexprlemloc  7946  suplocexprlemub  7948  suplocexprlemlub  7949  addcmpblnr  7964  mulcmpblnrlemg  7965  mulcmpblnr  7966  prsrlem1  7967  ltsrprg  7972  axmulcl  8091  ltmul1  8777  divdivdivap  8898  divmuleqap  8902  divsubdivap  8913  lt2mul2div  9064  ledivdiv  9075  lediv12a  9079  ssfzo12bi  10476  suprzcl2dc  10505  exbtwnz  10516  qbtwnre  10522  ioom  10526  seq3caopr  10763  seqcaoprg  10764  leexp2r  10861  hashunlem  11073  wrd2ind  11313  recvguniq  11578  rsqrmo  11610  fsum2dlemstep  12018  expcnvre  12087  fprod2dlemstep  12206  bezout  12605  qredeu  12692  pw2dvdseu  12763  oddpwdclemdvds  12765  pcqmul  12899  pcadd  12936  pockthg  12953  grprida  13493  issubmd  13580  ghmpreima  13876  unitgrp  14154  lmodprop2d  14386  lsspropdg  14469  neiint  14898  restbasg  14921  iscnp4  14971  cnpnei  14972  cnptopco  14975  blssps  15180  blss  15181  metequiv2  15249  xmetxpbl  15261  suplociccex  15378  dedekindicc  15386  limcimolemlt  15417  lgsquad2lem2  15840  2sqlem5  15877